proposition: Lemma morphim_bigcprod I r (P : pred I) (H : I -> {group gT}) G : G \subset D -> \big[cprod/1]_(i <- r | P i) H i = G -> \big[cprod/1]_(i <- r | P i) f @* H i = f @* G.
proof: Proof. elim/big_rec2: _ G => [|i fB B Pi def_fB] G sGD defG. by rewrite -defG morphim1. case/cprodP: defG (defG) => [[Hi Gi -> defB] _ _]; rewrite defB => defG. rewrite (def_fB Gi) //; first exact: morphim_cprod. by apply: subset_trans sGD; case/cprod_normal2: defG => _ /andP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)