cases hab
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hab : a = b ∨ a < b
hbc : b = c ∨ b < c
⊢ a = c ∨ a < c
case inl
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
h✝ : a = b
⊢ a = c ∨ a < c

case inr
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
h✝ : a < b
⊢ a = c ∨ a < c