proposition: Lemma nElemP n G E : reflect (exists p, E \in 'E_p^n(G)) (E \in 'E^n(G)).
proof: Proof. rewrite ['E^n(G)]big_mkord. apply: (iffP bigcupP) => [[[p /= _] _] | [p]]; first by exists p. case: n => [|n EpnE]; first by rewrite pnElem0; exists ord0; rewrite ?pnElem0. suffices lepG: p < #|G|.+1 by exists (Ordinal lepG). have:= EpnE; rewrite pnElemE ?(pnElem_prime EpnE) // !inE -andbA ltnS. case/and3P=> sEG _ oE; rewrite dvdn_leq // (dvdn_trans _ (cardSg sEG)) //. by rewrite (eqP oE) dvdn_exp. 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)