proposition: Lemma infinite_not_empty P : infinite P -> exists x, mem x P.
proof: Proof. intro P_inf. apply not_all_not_ex. intro h. assert (e : P [=] empty). fo. rewrite e in P_inf. gen finite_empty. fo. Qed.
imports: Coq(Basics Morphisms Setoid Lia) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil SetUtil FinSet FunUtil BoundNat IotaUtil EpsilonUtil)