sub_coe — Mathlib

English

For a,b ∈ ℕ⁺, the natural part of a - b equals a - b if b < a, otherwise 1.

Русский

Для любых a,b ∈ ℕ⁺ натуральная часть разности a − b равна a − b, если b < a, иначе 1.

LaTeX

$$$$ ((a - b) : \mathbb{N}_{>0}) : \mathbb{N} = \text{ite} (b < a) (a - b : \mathbb{N}) 1 $$$$

Lean4

theorem sub_coe (a b : ℕ+) : ((a - b : ℕ+) : ℕ) = ite (b < a) (a - b : ℕ) 1 :=
  by
  change (toPNat' _ : ℕ) = ite _ _ _
  split_ifs with h
  · exact toPNat'_coe (tsub_pos_of_lt h)
  · rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
    rfl

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