α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : NoMaxOrder α
⊢ a ⋖ succ a
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a = b → a ⋖ b
rintro rfl
no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : NoMaxOrder α
⊢ a ⋖ succ a
exact covby_succ _