proposition: Lemma cardinalO_unique : forall A : part_set E, cardinal A 0 -> forall m : nat, cardinal A m -> 0 = m.
proof: Proof. intros. inversion H0; auto with algebra. absurd (in_part x (empty E)); auto with algebra. apply in_part_comp_r with A; auto with algebra. apply in_part_comp_r with (add_part B x); auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop