intro cxy
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
⊢ (if x < y then lt else if x = y then eq else gt) = eq → x = y
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
cxy : (if x < y then lt else if x = y then eq else gt) = eq
⊢ x = y