proposition: Lemma approximant_can_be_any_size : forall A X:Ensemble U, ~ Finite U A -> forall n:nat, exists Y : _, cardinal U Y n /\ Approximant U A Y.
proof: Proof. intros A H' H'0 n; elim n. - exists (Empty_set U); auto with sets. - intros n0 H'1; elim H'1. intros x H'2. apply approximants_grow' with (X := x); tauto. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts Finite_sets_facts Image