proposition: Lemma abelem_pnElem p n G : p.-abelem G -> n <= logn p #|G| -> exists E, E \in 'E_p^n(G).
proof: Proof. case: n => [|n] abelG lt_nG; first by exists 1%G; rewrite pnElem0 set11. have p_pr: prime p by move: lt_nG; rewrite lognE; case: prime. case/(normal_pgroup (abelem_pgroup abelG)): lt_nG => // E [sEG _ oE]. by exists E; rewrite pnElemE // !inE oE sEG (abelemS sEG) /=. 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)