α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
ha : IsSuccLimit (succ a)
⊢ IsMax a
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
ha : ¬IsMax a
⊢ ¬IsSuccLimit (succ a)
contrapose! ha
no goals
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
ha : IsSuccLimit (succ a)
⊢ IsMax a
exact ha.isMax