proposition: Lemma prod_of_prods f g I: (cprodb I f) *c (cprodb I g) = cprodb I (fun i =>(f i) *c (g i)).
proof: Proof. pose h i j := variant C0 (f i) (g i) j. move: (cprod_An2 I C2 h). rewrite cprod2_pr0. have ->: cprodb I (h^~ C0) = cprodb I f. by rewrite/h; apply:cprodb_exten => i iI; rewrite variant_true1. have ->: cprodb I (h^~ C1) = cprodb I g. by rewrite/h; apply:cprodb_exten => i iI; rewrite variant_false1. move <-. by apply:cprodb_exten=> i iI;rewrite cprod2_pr0/h variant_true1 variant_false1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)