apply ConnectedLT.lt_of_lt_of_not_gt _ hb.left
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₂
α : Type u_1
inst✝ : ConnectedLT α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
h₁ : a₁ < b₁
⊢ a₂ < b₁