proposition: Lemma cardinal_comp_l : forall (A B : part_set E) (n : nat), Equal A B -> cardinal A n -> cardinal B n.
proof: Proof. intros. apply cardinal_comp with A n; auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop