sub_to_nat — Mathlib

English

For m,n ∈ Num, the Nat-cast of m−n equals the subtraction in Nat: ((m − n) : Num) : ℕ = m − n.

Русский

Для чисел Num: преобразование разности m−n в ℕ равно самой разности в ℕ: ((m − n) : Num) : ℕ = m − n.

LaTeX

$$$$\forall m,n:\mathrm{Num},\ ((m-n) : \mathbb{N}) = m - n.$$$$

Lean4

@[simp, norm_cast]
theorem sub_to_nat (m n) : ((m - n : Num) : ℕ) = m - n :=
  show (ofZNum _ : ℕ) = _ by rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]

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