proposition: Lemma def_pnElem p n G : 'E_p^n(G) = 'E_p(G) :&: 'E^n(G).
proof: Proof. apply/setP=> E; rewrite inE in_setI; apply: andb_id2l => /pElemP[sEG abelE]. apply/idP/nElemP=> [|[q]]; first by exists p; rewrite !inE sEG abelE. rewrite !inE -2!andbA => /and4P[_ /pgroupP qE _]. have [->|] := eqVneq E 1%G; first by rewrite cards1 !logn1. case/(pgroup_pdiv (abelem_pgroup abelE)) => p_pr pE _. by rewrite (eqnP (qE p p_pr pE)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)