proposition: Lemma morphim_coprime_bigdprod (I : finType) P (H : I -> {group gT}) G : G \subset D -> \big[dprod/1]_(i | P i) H i = G -> (forall i j, P i -> P j -> i != j -> coprime #|H i| #|H j|) -> \big[dprod/1]_(i | P i) f @* H i = f @* G.
proof: Proof. move=> sGD /bigdprodWcp defG coH; have def_fG := morphim_bigcprod sGD defG. by apply: bigcprod_coprime_dprod => // i j *; rewrite coprime_morph ?coH. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)