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)