proposition: Lemma bigdprod_nil I r (P : pred I) (A_ : I -> {set gT}) G : \big[dprod/1]_(i <- r | P i) A_ i = G -> (forall i, P i -> nilpotent (A_ i)) -> nilpotent G.
proof: Proof. move=> defG nilA; elim/big_rec: _ => [|i B Pi nilB] in G defG *. by rewrite -defG nilpotent1. have [[_ H _ defB] _ _ _] := dprodP defG. by rewrite (dprod_nil defG) nilA //= defB nilB. 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)