proposition: Lemma lcn_bigdprod n 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) 'L_n(F i) = 'L_n(G).
proof: Proof. elim/big_rec2: _ G => [_ <- | i A Z _ IH G dG]; first exact/esym/trivgP/lcn_sub. by rewrite -(lcn_dprod n dG); have [[_ H _ dH]] := dprodP dG; rewrite dH (IH H). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)