simp [ltOfOrd]
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.eq
⊢ ¬y < x
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.eq
⊢ ¬compare y x = Ordering.lt