English
For natural m,n, the cast of Int.subNatNat m n equals m − n in any AddGroupWithOne R.
Русский
Для натуральных m,n отображение Int.subNatNat m n в R даёт m − n.
LaTeX
$$$\mathrm{Int.subNatNat}\; m\; n \text{ cast} = m - n$$
Lean4
@[simp, norm_cast]
theorem cast_add : ∀ m n, ((m + n : ℤ) : R) = m + n
| (m : ℕ), (n : ℕ) => by simp [← Int.natCast_add]
| (m : ℕ), -[n+1] => by rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
| -[m+1], (n : ℕ) => by
rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add, add_assoc,
eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
| -[m+1], -[n+1] => by
rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ←
Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
