English
For all integers n, ZNum.ofInt'(n+1) = ZNum.ofInt'(n) + 1.
Русский
Для всех целых чисел n выполняется ZNum.ofInt'(n+1) = ZNum.ofInt'(n) + 1.
LaTeX
$$$$\forall n:\mathrm{Int},\ \mathrm{ZNum.ofInt'}(n+1) = \mathrm{ZNum.ofInt'}(n) + 1.$$$$
Lean4
theorem succ_ofInt' : ∀ n, ZNum.ofInt' (n + 1) = ZNum.ofInt' n + 1
| (n : ℕ) => by
change ZNum.ofInt' (n + 1 : ℕ) = ZNum.ofInt' (n : ℕ) + 1
dsimp only [ZNum.ofInt', ZNum.ofInt']
rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]
| -[0+1] => by
change ZNum.ofInt' 0 = ZNum.ofInt' (-[0+1]) + 1
dsimp only [ZNum.ofInt', ZNum.ofInt']
rw [ofNat'_succ, ofNat'_zero]; rfl
| -[(n + 1)+1] => by
change ZNum.ofInt' -[n+1] = ZNum.ofInt' -[(n + 1)+1] + 1
dsimp only [ZNum.ofInt', ZNum.ofInt']
rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ, @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
