match cmp : compare x y with
| .lt | .eq => decide
| .gt =>
  simp [ltOfOrd] at h
  have : compare y x = .lt := by rw [←symm, cmp]; decide
  rw [this] at h
  contradiction
α : Type
inst✝ : Order α
x y : α
h : ¬y < x
⊢ (compare x y).isLE = true
no goals