proposition: Lemma abelian_type_pgroup p b G : p.-group G -> \big[dprod/1]_(x <- b) <[x]> = G -> 1 \notin b -> perm_eq (abelian_type G) (map order b).
proof: Proof. rewrite perm_sym; move: b => b1 pG defG1 ntb1. have cGG: abelian G. elim: (b1) {pG}G defG1 => [_ <-|x b IHb G]; first by rewrite big_nil abelian1. rewrite big_cons; case/dprodP=> [[_ H _ defH]] <-; rewrite defH => cxH _. by rewrite abelianM cycle_abelian IHb. have p_bG b: \big[dprod/1]_(x <- b) <[x]> = G -> all (p_elt p) b. elim: b {defG1 cGG}G pG => //= x b IHb G pG; rewrite big_cons. case/dprodP=> [[_ H _ defH]]; rewrite defH andbC => defG _ _. by rewrite -defG pgroupM in pG; case/andP: pG => p_x /IHb->. have [b2 defG2 def_t] := abelian_structure cGG. have ntb2: 1 \notin b2. apply: contraL (abelian_type_gt1 G) => b2_1. rewrite -def_t -has_predC has_map. by apply/hasP; exists 1; rewrite //= order1. rewrite -{}def_t; apply/allP=> m; rewrite -map_cat => /mapP[x b_x def_m]. have{ntb1 ntb2} ntx: x != 1. by apply: contraL b_x; move/eqP->; rewrite mem_cat negb_or ntb1 ntb2. have p_x: p.-elt x by apply: allP (x) b_x; rewrite all_cat !p_bG. rewrite -cycle_eq1 in ntx; have [p_pr _ [k ox]] := pgroup_pdiv p_x ntx. apply/eqnP; rewrite {m}def_m orderE ox !count_map. pose cnt_p k := count [pred x : gT | logn p #[x] > k]. have cnt_b b: \big[dprod/1]_(x <- b) <[x]> = G -> count [pred x | #[x] == p ^ k.+1]%N b = cnt_p k b - cnt_p k.+1 b. - move/p_bG; elim: b => //= _ b IHb /andP[/p_natP[j ->] /IHb-> {IHb}]. rewrite eqn_leq !leq_exp2l ?prime_gt1 // -eqn_leq pfactorK //. case: (ltngtP k.+1) => // _ {j}; rewrite subSn // add0n. by elim: b => //= y b IHb; rewrite leq_add // ltn_neqAle; case: (~~ _). by rewrite !cnt_b // /cnt_p !(@count_logn_dprod_cycle _ _ _ G). 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)