succ_le_succ — Mathlib

English

If a ≤ b then succ(a) ≤ succ(b).

Русский

Если a ≤ b, то succ(a) ≤ succ(b).

LaTeX

$$$a \\le b \\Rightarrow \\operatorname{succ}(a) \\le \\operatorname{succ}(b)$$$

Lean4

@[simp, mono, gcongr]
theorem succ_le_succ (h : a ≤ b) : succ a ≤ succ b :=
  by
  by_cases hb : IsMax b
  · by_cases hba : b ≤ a
    · exact (hb <| hba.trans <| le_succ _).trans (le_succ _)
    · exact succ_le_of_lt ((h.lt_of_not_ge hba).trans_le <| le_succ b)
  · rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]
    apply lt_succ_of_le_of_not_isMax h hb

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