proposition: Lemma pseries_norm2 pi1s pi2s gT (G : {group gT}) : pseries pi2s G \subset 'N(pseries pi1s G).
proof: Proof. by rewrite gFsub_trans ?gFnorm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)