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