add_succ — Mathlib

English

For all m,n in PosNum, m + succ n = succ (m + n).

Русский

Для любых m,n из PosNum справедливо m + succ n = succ (m + n).

LaTeX

$$$\\forall m,n:\\mathrm{PosNum},\\; m + \\mathrm{succ} n = \\mathrm{succ}(m + n)$$$

Lean4

theorem add_succ : ∀ m n : PosNum, m + succ n = succ (m + n)
  | 1, b => by simp [one_add]
  | bit0 a, 1 => congr_arg bit0 (add_one a)
  | bit1 a, 1 => congr_arg bit1 (add_one a)
  | bit0 _, bit0 _ => rfl
  | bit0 a, bit1 b => congr_arg bit0 (add_succ a b)
  | bit1 _, bit0 _ => rfl
  | bit1 a, bit1 b => congr_arg bit1 (add_succ a b)

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