proposition: Lemma csumA a b c: a +c (b +c c) = (a +c b) +c c.
proof: Proof. move: a b c. have aux: (forall u v w a b c, v <> u-> u <> w -> w <> v -> a +c (b +c c) = cardinal ((a *s1 u) \cup ((b *s1 v) \cup (c *s1 w)))). move=> u v w a b c vu uw wv. rewrite - (card_card (CS_sum2 a (b +c c))) (disjointU2_pr3 a (b +c c) vu). apply: Eqc_disjointU2; fprops. apply: disjoint_pr; move=> z; move/setX_P => [_ _ /set1_P pa] /setU2_P [] /setX_P [_ _ /set1_P]; rewrite pa => //; apply:nesym => //. aw; exact: (disjointU2_pr3 b c wv). move: C2_ne_C01 => [/nesym ne3 ne2] a b c. rewrite - (csumC c (a +c b)). rewrite(aux _ _ _ a b c C1_ne_C0 ne3 ne2) (aux _ _ _ c a b ne3 ne2 C1_ne_C0 ). by rewrite setU2_A setU2_C. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)