unfold compareOfLT
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
⊢ compareOfLT x y ≠ gt → compareOfLT y z ≠ gt → compareOfLT x z ≠ gt
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
⊢ (if x < y then lt else if y < x then gt else eq) ≠ gt →
    (if y < z then lt else if z < y then gt else eq) ≠ gt → (if x < z then lt else if z < x then gt else eq) ≠ gt