proposition: Lemma count_logn_dprod_cycle p n b G : \big[dprod/1]_(x <- b) <[x]> = G -> count [pred x | logn p #[x] > n] b = logn p #|'Ohm_n.+1(G) : 'Ohm_n(G)|.
proof: Proof. have sOn1 H: 'Ohm_n(H) \subset 'Ohm_n.+1(H) by apply: Ohm_leq. pose lnO i (A : {set gT}) := logn p #|'Ohm_i(A)|. have lnO_le H: lnO n H <= lnO n.+1 H. by rewrite dvdn_leq_log ?cardG_gt0 // cardSg ?sOn1. have lnOx i A B H: A \x B = H -> lnO i A + lnO i B = lnO i H. move=> defH; case/dprodP: defH (defH) => {A B}[[A B -> ->]] _ _ _ defH. rewrite /lnO; case/dprodP: (Ohm_dprod i defH) => _ <- _ tiOAB. by rewrite TI_cardMg ?lognM. rewrite -divgS //= logn_div ?cardSg //= -/(lnO _ _) -/(lnO _ _). elim: b G => [_ <-|x b IHb G] /=. by rewrite big_nil /lnO !(trivgP (Ohm_sub _ _)) subnn. rewrite /= big_cons => defG; rewrite -!(lnOx _ _ _ _ defG) subnDA. case/dprodP: defG => [[_ H _ defH] _ _ _] {G}; rewrite defH (IHb _ defH). symmetry; do 2!rewrite addnC -addnBA ?lnO_le //; congr (_ + _). pose y := x.`_p; have p_y: p.-elt y by rewrite p_elt_constt. have{lnOx} lnOy i: lnO i <[x]> = lnO i <[y]>. have cXX := cycle_abelian x. have co_yx': coprime #[y] #[x.`_p^'] by rewrite !order_constt coprime_partC. have defX: <[y]> \x <[x.`_p^']> = <[x]>. rewrite dprodE ?coprime_TIg //. by rewrite -cycleM ?consttC //; apply: (centsP cXX); apply: mem_cycle. by apply: (sub_abelian_cent2 cXX); rewrite cycle_subG mem_cycle. rewrite -(lnOx i _ _ _ defX) addnC {1}/lnO lognE. case: and3P => // [[p_pr _ /idPn[]]]; rewrite -p'natE //. exact: pgroupS (Ohm_sub _ _) (p_elt_constt _ _). rewrite -logn_part -order_constt -/y !{}lnOy /lnO !(Ohm_p_cycle _ p_y). case: leqP => [| lt_n_y]. by rewrite -subn_eq0 -addn1 subnDA => /eqP->; rewrite subnn. rewrite -!orderE -(subSS n) subSn // expnSr expgM. have p_pr: prime p by move: lt_n_y; rewrite lognE; case: prime. set m := (p ^ _)%N; have m_gt0: m > 0 by rewrite expn_gt0 prime_gt0. suffices p_ym: p %| #[y ^+ m]. rewrite -logn_div ?orderXdvd // (orderXdiv p_ym) divnA // mulKn //. by rewrite logn_prime ?eqxx. rewrite orderXdiv ?pfactor_dvdn ?leq_subr // -(dvdn_pmul2r m_gt0). by rewrite -expnS -subSn // subSS divnK pfactor_dvdn ?leq_subr. 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)