proposition: Lemma cardinal_unique : forall (n : nat) (A : part_set E), cardinal A n -> forall m : nat, cardinal A m -> n = m.
proof: Proof. intros n A c. apply cardinal_ind2 with (P := fun (n : nat) (A : part_set E) (c : cardinal A n) => forall m : nat, cardinal A m -> n = m); auto with algebra. exact cardinalO_unique. intros n0 H A0 B x H0 H1 c' m. case m; intros. absurd (in_part x (empty E)); auto with algebra. apply in_part_comp_r with A0; auto with algebra. apply in_part_comp_r with (add_part B x); auto with algebra. cut (cardinal B n0). cut (cardinal B n1). intros. cut (n0 = n1). auto with algebra. apply H with B; auto with algebra. apply cardinal_S with A0 x; auto with algebra. apply cardinal_S with A0 x; auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop