α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
h : IsSuccLimit (succ b)
⊢ False
α : Type u_1
inst✝² : Preorder α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
h : IsSuccLimit a
b : α
⊢ succ b ≠ a
rintro rfl
no goals
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
h : IsSuccLimit (succ b)
⊢ False
exact not_isMax _ h.isMax