theorem Finset.Iio_eventually_nonempty (β : Type u_1) [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] [Nontrivial β] : ∃ (b : β), ∀ n ≥ b, (Iio n).Nonempty

theorem Finset.Iio_eventually_card_ne_zero (β : Type u_1) [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] [Nontrivial β] : ∃ (b : β), ∀ n ≥ b, (Iio n).card ≠ 0

theorem Set.Iio_eventually_ncard_ne_zero (β : Type u_1) [PartialOrder β] [LocallyFiniteOrder β] [OrderBot β] [Nontrivial β] : ∃ (b : β), ∀ n ≥ b, (Iio n).ncard ≠ 0