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