ofNat'_succ — Mathlib

English

For every n, the successor under the ofNat' encoding satisfies ofNat'(n+1) = ofNat'(n) + 1.

Русский

Для каждого n сохранение под прямым переходом: ofNat'(n+1) = ofNat'(n) + 1.

LaTeX

$$$\\forall n,\\ ofNat'(n+1) = ofNat'(n) + 1$$$

Lean4

theorem ofNat'_succ : ∀ {n}, ofNat' (n + 1) = ofNat' n + 1 :=
  @(Nat.binaryRec (by simp [zero_add]) fun b n ih => by
      cases b
      · erw [ofNat'_bit true n, ofNat'_bit]
        simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]
      · rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add], ofNat'_bit, ofNat'_bit, ih]
        simp only [cond, add_one, bit1_succ])

Похожие утверждения