no goals
ι : Type ?u.818
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : DenselyOrdered α
⊢ Finset.Nonempty (Ioo a b) ↔ a < b
rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]