no goals
ι : Type ?u.2143
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b
rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]