add_ofNat' — Mathlib

English

For all m,n, ofNat'(m+n) = ofNat'm + ofNat'n. The encoding preserves addition.

Русский

Для всех m,n: ofNat'(m+n) = ofNat'm + ofNat'n. Кодирование сохраняет сложение.

LaTeX

$$$\\forall m,n,\\ operatorname{Num}.ofNat'(m+n) = \\operatorname{Num}.ofNat'(m) + \\operatorname{Num}.ofNat'(n)$$$

Lean4

@[simp]
theorem add_ofNat' (m n) : Num.ofNat' (m + n) = Num.ofNat' m + Num.ofNat' n :=
  by
  induction n
  · simp only [Nat.add_zero, ofNat'_zero, add_zero]
  · simp only [Nat.add_succ, Nat.add_zero, ofNat'_succ, add_one, add_succ, *]

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