proposition: Lemma card_Add_gen : forall (A:Ensemble U) (x:U) (n n':nat), cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
proof: Proof. intros A x n n' H0 H1. elim (classic (In U A x)); intro H2. - rewrite (Non_disjoint_union _ _ _ H2) in H1. rewrite (cardinal_unicity _ _ H0 _ H1). apply Nat.le_succ_diag_r. - apply Nat.eq_le_incl. apply cardinal_unicity with (X := Add U A x); auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat