English
For every ZNum n, (Int.toNat? n) equals the Nat-cast of ofZNum' n; i.e. (castNum (Num.ofZNum' n)) = (castZNum n).toNat.
Русский
Для каждого ZNum n выполняется: преобразование в Nat через Nat.toNat? n совпадает с приведением Num.ofZNum' n к Nat.
LaTeX
$$$$\forall n:\mathrm{ZNum},\ (\mathrm{castNum}(\mathrm{Num.ofZNum'}(n))) = (\mathrm{castZNum}(n)).toNat.$$$$
Lean4
theorem ofZNum_toNat : ∀ n : ZNum, (ofZNum n : ℕ) = Int.toNat n
| 0 => rfl
| ZNum.pos p => show _ = Int.toNat p by rw [← PosNum.to_nat_to_int p]; rfl
| ZNum.neg p => (congr_arg fun x => Int.toNat (-x)) <| show ((p.pred' + 1 : ℕ) : ℤ) = p by rw [← succ'_to_nat]; simp
