no goals
α : Type u_1
β : Type ?u.6902
inst✝ : Preorder α
a b : α
h✝ : Compares eq a b
x✝ : b ≤ a
h : eq = lt
⊢ False
injection h
no goals
α : Type u_1
β : Type ?u.6902
inst✝ : Preorder α
a b : α
h✝ : Compares gt a b
x✝ : b ≤ a
h : gt = lt
⊢ False
injection h