no goals
ι : Type ?u.49166
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioo a b ⊆ Ioi a
simpa [← coe_subset] using Set.Ioo_subset_Ioi_self