proposition: Lemma cpow_prod b f: (cprod f) ^c b = cprodb (domain f) (fun i => (Vg f i) ^c b).
proof: Proof. move: (cprod_An2 (domain f) b (fun i j=> Vg f i )). set A := cprodb _ _. have -> : cprodb (domain f) (fun i => Vg f i ^c b)= A. by apply: cprodb_exten => i idf; rewrite - cprod_of_same. by move ->; rewrite - cprod_of_same;apply:cprodb_exten => i _; rewrite cprod_gr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)