proposition: Lemma cardinal_is_functional : forall (X:Ensemble U) (c1:nat), cardinal U X c1 -> forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
proof: Proof. intros X c1 H'; elim H'. - intros Y c2 H'0 <-; now apply cardinal_Empty. - clear H' c1 X. intros X n H' H'0 x H'1 Y c2 H'2. elim H'2. + intro H'3; now elim (not_Empty_Add U X x). + clear H'2 c2 Y. intros X0 c2 H'2 _ x0 H'4 H'5. apply f_equal. assert (H'6 : In U (Add U X x) x) by apply Add_intro2. rewrite H'5 in H'6. destruct (Add_inv _ _ _ _ H'6) as [H'7 | <-]. * apply H'0 with (Y := Subtract U (Add U X0 x0) x). -- rewrite <- Nat.pred_succ; apply card_soustr_1; auto with sets. -- rewrite <- H'5; auto with sets. * apply (H'0 _ _ H'2 (Simplify_add _ _ _ _ H'1 H'4 H'5)). Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat