proposition: Lemma cardinal_invert : forall (X:Ensemble U) (p:nat), cardinal U X p -> match p with | O => X = Empty_set U | S n => exists A : _, (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n) end.
proof: Proof. induction 1; simpl; auto. exists A; exists x; auto. Qed.
imports: Ensembles Constructive_sets