proposition: Lemma cprodDr a b c: a *c (b +c c) = (a *c b) +c (a *c c).
proof: Proof. have aux: forall a b c, (a \times (b \times c)) =c ((a *c b) \times c). move=> a' b' c'. by rewrite - cprod2_pr1 - cprod2cr -2!cprod2_pr1 cprodA. rewrite cprod2_pr1 -(card_card(CS_sum2 (a *c b) (a *c c))). rewrite - cprod2_pr2 (disjointU2_pr3 b c C1_ne_C0). rewrite cprod2_pr2 set2_UXr. rewrite (disjointU2_pr3 (a *c b) (a *c c) C1_ne_C0). apply: Eqc_disjointU2. - by apply: disjointU2_pr0; apply: disjointU2_pr; fprops. - by apply: disjointU2_pr; fprops. - by apply: aux. - by apply: aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)