lt_add_one_iff_lt — Mathlib

English

For x ≠ ⊤, x < y + 1 ⇔ x ≤ y.

Русский

Для x ≠ ⊤, x < y + 1 эквивалентно x ≤ y.

LaTeX

$$$ \forall x,y: \mathrm{PartENat}, x \neq \top \Rightarrow (x < y + 1 \iff x \le y)$$$

Lean4

theorem lt_add_one_iff_lt {x y : PartENat} (hx : x ≠ ⊤) : x < y + 1 ↔ x ≤ y :=
  by
  refine ⟨le_of_lt_add_one, fun h => ?_⟩
  rcases ne_top_iff.mp hx with ⟨m, rfl⟩
  induction y using PartENat.casesOn
  · rw [top_add]
    apply natCast_lt_top
  intro h
  exact_mod_cast Nat.lt_succ_of_le (by norm_cast at h)

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