apply Or.inr
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true ∨ (compare y x).isLE = true
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ (compare y x).isLE = true