natCast_sub — Mathlib

English

For natural m,n, ((m − n) : Ordinal) = m − n.

Русский

Для натуральных m,n, (m − n) как ординал равен m − n.

LaTeX

$$$((m - n : \mathbb{N}) : \mathrm{Ordinal}) = m - n$$$

Lean4

@[simp, norm_cast]
theorem natCast_sub (m n : ℕ) : ((m - n : ℕ) : Ordinal) = m - n :=
  by
  rcases le_total m n with h | h
  · rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]
  ·
    rw [← add_left_cancel_iff (a := ↑n), ← Nat.cast_add, add_tsub_cancel_of_le h,
      Ordinal.add_sub_cancel_of_le (Nat.cast_le.2 h)]

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