cases hor
case refl
α : Type u_1
inst✝ : LinearLT α
a : α
hor : a < a ∨ a > a
⊢ False
case refl.inl
α : Type u_1
inst✝ : LinearLT α
a : α
h✝ : a < a
⊢ False

case refl.inr
α : Type u_1
inst✝ : LinearLT α
a : α
h✝ : a > a
⊢ False