proposition: Lemma cprod2Dn a I f: a *c (csumb I f) = csumb I (fun i => a *c (f i)).
proof: Proof. rewrite cprod2_pr1 /csum cprod2_pr2 /csumb /csum. rewrite/disjointU distrib_prod2_sum /disjointU_fam; aw. apply: Eqc_disjointU => //. - split => //; aww;move=> i idf; rewrite !LgV //. by rewrite - cprod2_pr2 cprod2_pr1; aw; rewrite cprod2_pr2. - apply: mutually_disjoint_prop2 => i j y idf jdf; rewrite !LgV//. move => /setX_P [_ _ /setX_P [_ _ /set1_P <-]]. by move => /setX_P [_ _ /setX_P [_ _ /set1_P <-]]. - apply: mutually_disjoint_prop3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)