proposition: Lemma csum2_pr2 a b a' b': a =c a' -> b =c b' -> a +c b = a' +c b'.
proof: Proof. move=> eaa ebb. rewrite -(card_card (CS_sum2 a b)) -(card_card (CS_sum2 a' b')). rewrite (disjointU2_pr3 a b C1_ne_C0)(disjointU2_pr3 a' b' C1_ne_C0). apply:Eqc_disjointU2; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)