proposition: Lemma card_subcent_extraspecial U : U \subset G -> #|'C_G(U)| = (#|'Z(G) :&: U| * #|G : U|)%N.
proof: Proof. move=> sUG; rewrite setIAC (setIidPr sUG). have [m leUm] := ubnP #|U|; elim: m => // m IHm in U leUm sUG *. have [cUG | not_cUG]:= orP (orbN (G \subset 'C(U))). by rewrite !(setIidPl _) ?Lagrange // centsC. have{not_cUG} [x Gx not_cUx] := subsetPn not_cUG. pose W := 'C_U[x]; have sCW_G: 'C_G(W) \subset G := subsetIl G _. have maxW: maximal W U by rewrite subcent1_extraspecial_maximal // inE not_cUx. have nsWU: W <| U := p_maximal_normal (pgroupS sUG pG) maxW. have ltWU: W \proper U by apply: maxgroupp maxW. have [sWU [u Uu notWu]] := properP ltWU; have sWG := subset_trans sWU sUG. have defU: W * <[u]> = U by rewrite (mulg_normal_maximal nsWU) ?cycle_subG. have iCW_CU: #|'C_G(W) : 'C_G(U)| = p. rewrite -defU centM cent_cycle setIA /=; rewrite inE Uu cent1C in notWu. apply: p_maximal_index (pgroupS sCW_G pG) _. apply: subcent1_extraspecial_maximal sCW_G _. rewrite inE andbC (subsetP sUG) //= -sub_cent1. by apply/subsetPn; exists x; rewrite // inE Gx -sub_cent1 subsetIr. apply/eqP; rewrite -(eqn_pmul2r p_gt0) -{1}iCW_CU Lagrange ?setIS ?centS //. rewrite IHm ?(leq_trans (proper_card ltWU)) // -setIA -mulnA. rewrite -(Lagrange_index sUG sWU) (p_maximal_index (pgroupS sUG pG)) //=. by rewrite -cent_set1 (setIidPr (centS _)) ?sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)