next =>
  split at cxy
  next => assumption
  next => contradiction
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝ : ¬x < y
cxy : (if x = y then eq else gt) = eq
⊢ x = y
no goals