proposition: Lemma cardinal_unicity : forall (X:Ensemble U) (n:nat), cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
proof: Proof. intros X ? ? ? ?; now apply cardinal_is_functional with X X. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat