proposition: Lemma normal_pgroup r P N : p.-group P -> N <| P -> r <= logn p #|N| -> exists Q : {group gT}, [/\ Q \subset N, Q <| P & #|Q| = (p ^ r)%N].
proof: Proof. elim: r gT P N => [|r IHr] gTr P N pP nNP le_r. by exists (1%G : {group gTr}); rewrite sub1G normal1 cards1. have [NZ_1 | ntNZ] := eqVneq (N :&: 'Z(P)) 1. by rewrite (TI_center_nil (pgroup_nil pP)) // cards1 logn1 in le_r. have: p.-group (N :&: 'Z(P)) by apply: pgroupS pP; rewrite /= setICA subsetIl. case/pgroup_pdiv=> // p_pr /Cauchy[// | z]. rewrite -cycle_subG !subsetI => /and3P[szN szP cPz] ozp _. have{cPz} nzP: P \subset 'N(<[z]>) by rewrite cents_norm // centsC. have: N / <[z]> <| P / <[z]> by rewrite morphim_normal. case/IHr=> [||Qb [sQNb nQPb]]; first exact: morphim_pgroup. rewrite card_quotient ?(subset_trans (normal_sub nNP)) // -ltnS. apply: (leq_trans le_r); rewrite -(Lagrange szN) [#|_|]ozp. by rewrite lognM // ?prime_gt0 // logn_prime ?eqxx. case/(inv_quotientN _): nQPb sQNb => [|Q -> szQ nQP]; first exact/andP. have nzQ := subset_trans (normal_sub nQP) nzP. rewrite quotientSGK // card_quotient // => sQN izQ. by exists Q; split=> //; rewrite expnS -izQ -ozp Lagrange. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)