proposition: Lemma nElem1P G E : reflect (E \subset G /\ exists2 p, prime p & #|E| = p) (E \in 'E^1(G)).
proof: Proof. apply: (iffP nElemP) => [[p pE] | [sEG [p p_pr oE]]]. have p_pr := pnElem_prime pE; rewrite pnElemE // !inE -andbA in pE. by case/and3P: pE => -> _ /eqP; split; last exists p. exists p; rewrite pnElemE // !inE sEG oE eqxx abelemE // -oE exponent_dvdn. by rewrite cyclic_abelian // prime_cyclic // oE. 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)