add_succ — Mathlib

English

For all m,n : Num, m + succ n = succ (m + n).

Русский

Для всех m,n : Num выполняется m + succ n = succ (m + n).

LaTeX

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

Lean4

theorem add_succ : ∀ m n : Num, m + succ n = succ (m + n)
  | 0, n => by simp [zero_add]
  | pos p, 0 => show pos (p + 1) = succ (pos p + 0) by rw [PosNum.add_one, add_zero, succ, succ']
  | pos _, pos _ => congr_arg pos (PosNum.add_succ _ _)

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