proposition: Lemma nilpotent1 : nilpotent [1 gT].
proof: Proof. by apply/forall_inP=> H; rewrite commG1 setIid -subG1. 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)