simp [leOfOrd, cmp] at h
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.gt
⊢ ¬y < x
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
h : Ordering.gt.isLE = true
⊢ ¬y < x