ofZNum'_toNat — Mathlib

English

For m,n ∈ PosNum, cast of m.sub' n to ZNum equals castPosNum m minus castPosNum n in ZNum.

Русский

Для m,n ∈ PosNum приведение m.sub' n к ZNum равно приведиению m и n к ZNum и их разности.

LaTeX

$$$$\forall m,n:\mathrm{PosNum},\ \mathrm{castZNum}(m.\mathrm{sub'}\text{)}) = \mathrm{castPosNum}(m) - \mathrm{castPosNum}(n).$$$$

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

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