proposition: Lemma cardinal_finite : forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
proof: Proof. induction 1; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat