succ_le_succ_iff_of_not_isMax — Mathlib

English

If a and b are not maximal, then succ a ≤ succ b iff a ≤ b.

Русский

Если a и b не максимальны, то succ a ≤ succ b эквивалено a ≤ b.

LaTeX

$$¬IsMax a \rightarrow ¬IsMax b \rightarrow (\operatorname{succ} a \le \operatorname{succ} b \iff a \le b)$$

Lean4

theorem succ_le_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) : succ a ≤ succ b ↔ a ≤ b := by
  rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]

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