α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
b : α
inst✝ : NoMinOrder α
⊢ pred b ⋖ b
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred b = a → a ⋖ b
rintro rfl
no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
b : α
inst✝ : NoMinOrder α
⊢ pred b ⋖ b
exact pred_covby _