proposition: Lemma cardinal_comp : forall (A B : part_set E) (n m : nat), Equal A B -> n = m -> cardinal A n -> cardinal B m.
proof: Proof. intros. inversion H1. rewrite <- H0. rewrite <- H4. apply cardinal_empty. apply Trans with A; auto with algebra. rewrite <- H0. rewrite <- H6. apply cardinal_add with B0 x; auto with algebra. apply Trans with A; auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop