cast_subNatNat — Mathlib

English

For natural m,n, the cast of Int.subNatNat m n equals m.cast − n.cast in any AddGroupWithOne R.

Русский

Для натуральных m,n отображение Int.subNatNat m n в R равно m.cast − n.cast.

LaTeX

$$$\mathrm{Int.subNatNat}\; m\; n \;\text{cast} = m.cast - n.cast$$

Lean4

@[simp, norm_cast]
theorem cast_subNatNat (m n) : ((Int.subNatNat m n : ℤ) : R) = m - n :=
  by
  unfold subNatNat
  cases e : n - m
  · simp [Nat.le_of_sub_eq_zero e]
  · rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]

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