case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ succ a ≤ succ b
by_cases hb : IsMax b
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b
by_cases hba : b ≤ a
no goals
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b
exact (hb <| hba.trans <| le_succ _).trans (le_succ _)
no goals
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b
exact succ_le_of_lt ((h.lt_of_not_le hba).trans_le <| le_succ b)
no goals
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b
rwa [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h, lt_succ_iff_of_not_isMax hb]