α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
h : IsSuccLimit (succ a)
H : ¬IsMax a
⊢ False
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
h : IsSuccLimit (succ a)
⊢ IsMax a
by_contra H
no goals
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
h : IsSuccLimit (succ a)
H : ¬IsMax a
⊢ False
exact h a (covby_succ_of_not_isMax H)