proposition: Lemma csum2_pr5 a b: disjoint a b -> cardinal (a \cup b) = a +c b.
proof: Proof. rewrite -(card_card (CS_sum2 a b)) (disjointU2_pr3 a b C1_ne_C0). move => dab; apply: (Eqc_disjointU2 dab);aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)