case inr haltb =>
  apply Or.inr
  cases hbc
  case inl hbeqc => cases hbeqc; exact haltb
  case inr hbltc => exact trans haltb hbltc
α : Type u_1
inst✝ : LawfulLT α
a b c : α
hbc : b = c ∨ b < c
haltb : a < b
⊢ a = c ∨ a < c
no goals