English
The cast of the subtraction operation on PosNum coincides with ordinary subtraction: (sub' m n : α) = m − n for any α with AddGroupWithOne.
Русский
Пусть m и n — PosNum. Приведение операции вычитания через sub' совпадает с обычной разностью: (sub' m n : α) = m − n для любого α со структурой AddGroupWithOne.
LaTeX
$$$$\forall \alpha\ [\text{AddGroupWithOne } \alpha],\ \forall m,n:\mathrm{PosNum},\ (\mathrm{sub}'\ m\ n:\alpha) = m - n.$$$$
Lean4
@[simp, norm_cast]
theorem cast_to_int [AddGroupWithOne α] : ∀ n : ZNum, ((n : ℤ) : α) = n
| 0 => by rw [cast_zero, cast_zero, Int.cast_zero]
| pos p => by rw [cast_pos, cast_pos, PosNum.cast_to_int]
| neg p => by rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]
