nat_le — Mathlib

English

The relation ≤ on natural numbers is PrimrecRel.

Русский

Отношение ≤ на натуральных числах является PrimrecRel.

LaTeX

$$$ PrimrecRel ((\cdot \le \cdot) : \mathbb{N} \times \mathbb{N} \rightarrow \mathsf{Prop})$$$

Lean4

theorem nat_le : PrimrecRel ((· ≤ ·) : ℕ → ℕ → Prop) :=
  Primrec₂.primrecRel
    ((nat_casesOn nat_sub (const true) (const false).to₂).of_eq fun p =>
      by
      dsimp [swap]
      rcases e : p.1 - p.2 with - | n
      · simp [Nat.sub_eq_zero_iff_le.1 e]
      · simp [not_le.2 (Nat.lt_of_sub_eq_succ e)])

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