English
For m,n ∈ PosNum, cast of m.sub' n to α equals castPosNum m minus castPosNum n in α.
Русский
Для m,n ∈ PosNum, приведение m.sub' n к α равно различию приведения m и n в α.
LaTeX
$$$$\forall \alpha\ [\text{AddGroupWithOne } \alpha],\ \forall m,n:\mathrm{PosNum},\ \operatorname{castZNum}(m).\text{sub'} = \mathrm{castPosNum}(m) - \mathrm{castPosNum}(n).$$$$
Lean4
theorem cast_sub' [AddGroupWithOne α] : ∀ m n : PosNum, (sub' m n : α) = m - n
| a, 1 => by
rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]
simp
| 1, b =>
by
rw [one_sub', Num.cast_toZNumNeg, ← neg_sub, neg_inj, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]
simp
| bit0 a, bit0 b => by
rw [sub', ZNum.cast_bit0, cast_sub' a b]
have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b) := by simp [add_left_comm]
simpa [sub_eq_add_neg] using this
| bit0 a, bit1 b => by
rw [sub', ZNum.cast_bitm1, cast_sub' a b]
have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b) : ℤ) := by simp [add_comm, add_left_comm]
simpa [sub_eq_add_neg] using this
| bit1 a, bit0 b => by
rw [sub', ZNum.cast_bit1, cast_sub' a b]
have : ((-b + (a + (-b + 1)) : ℤ) : α) = (a + 1 + (-b + -b) : ℤ) := by simp [add_comm, add_left_comm]
simpa [sub_eq_add_neg] using this
| bit1 a, bit1 b => by
rw [sub', ZNum.cast_bit0, cast_sub' a b]
have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]
simpa [sub_eq_add_neg] using this
