proposition: Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
proof: Proof. intros m Cm. inversion Cm as [|X n _ x _ H]; [ reflexivity | ]. symmetry in H. now apply not_Empty_Add in H. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat