proposition: Lemma card_p1Elem_pnElem p n A E : E \in 'E_p^n(A) -> #|'E_p^1(E)| = (\sum_(i < n) p ^ i)%N.
proof: Proof. case/pnElemP=> _ {A} abelE dimE; have [pE cEE _] := and3P abelE. have [E1 | ntE] := eqsVneq E 1. rewrite -dimE E1 cards1 logn1 big_ord0 eq_card0 // => X. by rewrite !inE subG1 trivg_card1; case: eqP => // ->; rewrite logn1 andbF. have [p_pr _ _] := pgroup_pdiv pE ntE; have p_gt1 := prime_gt1 p_pr. apply/eqP; rewrite -(@eqn_pmul2l (p - 1)) ?subn_gt0 // subn1 -predn_exp. have groupD1_inj: injective (fun X => (gval X)^#). apply: can_inj (@generated_group _) _ => X. by apply: val_inj; rewrite /= genD1 ?group1 ?genGid. rewrite -dimE -card_pgroup // (cardsD1 1 E) group1 /= mulnC. rewrite -(card_imset _ groupD1_inj) eq_sym. apply/eqP; apply: card_uniform_partition => [X'|]. case/imsetP=> X; rewrite pnElemE // expn1 => /setIdP[_ /eqP <-] ->. by rewrite (cardsD1 1 X) group1. apply/and3P; split; last 1 first. - apply/imsetP=> [[X /card_p1Elem oX X'0]]. by rewrite -oX (cardsD1 1) -X'0 group1 cards0 in p_pr. - rewrite eqEsubset; apply/andP; split. by apply/bigcupsP=> _ /imsetP[X /pnElemP[sXE _ _] ->]; apply: setSD. apply/subsetP=> x /setD1P[ntx Ex]. apply/bigcupP; exists <[x]>^#; last by rewrite !inE ntx cycle_id. apply/imsetP; exists <[x]>%G; rewrite ?p1ElemE // !inE cycle_subG Ex /=. by rewrite -orderE (abelem_order_p abelE). apply/trivIsetP=> _ _ /imsetP[X EpX ->] /imsetP[Y EpY ->]; apply/implyP. rewrite (inj_eq groupD1_inj) -setI_eq0 -setDIl setD_eq0 subG1. by rewrite (sameP eqP (TIp1ElemP EpX EpY)) implybb. 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)