le_succ_iff_eq_or_le — Mathlib

English

For all a, b in a linear order with succ, a ≤ succ(b) holds precisely when either a = succ(b) or a ≤ b.

Русский

Для всех a, b в линейном порядке с succ верно: a ≤ succ(b) тогда и только если либо a = succ(b), либо a ≤ b.

LaTeX

$$$a \leq \operatorname{succ} b \;\Leftrightarrow\; a = \operatorname{succ} b \;\lor\; a \leq b$$$

Lean4

theorem le_succ_iff_eq_or_le : a ≤ succ b ↔ a = succ b ∨ a ≤ b :=
  by
  by_cases hb : IsMax b
  · rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]
  · rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]

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