proposition: Lemma finite_cardinal : forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n.
proof: Proof. induction 1 as [| A _ [n H]]. - exists 0; auto with sets. - exists (S n); auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat