proposition: Lemma center_bigdprod I r P (F: I -> {set gT}) G : \big[dprod/1]_(i <- r | P i) F i = G -> \big[dprod/1]_(i <- r | P i) 'Z(F i) = 'Z(G).
proof: Proof. elim/big_ind2: _ G => [_ <-|A B C D IHA IHB G dG|_ _ G ->]; rewrite ?center1 //. case/dprodP: dG IHA IHB (dG) => [[H K -> ->] _ _ _] IHH IHK dG. by rewrite (IHH H) // (IHK K) // (center_dprod dG). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)