proposition: Lemma cent1_extraspecial_maximal x : x \in G -> x \notin 'Z(G) -> maximal 'C_G[x] G.
proof: Proof. move=> Gx notZx; pose f y := [~ x, y]; have [[_ defG'] prZ] := esG. have{defG'} fZ y: y \in G -> f y \in 'Z(G). by move=> Gy; rewrite -defG' mem_commg. have fM: {in G &, {morph f : y z / y * z}}%g. move=> y z Gy Gz; rewrite {1}/f commgMJ conjgCV -conjgM (conjg_fixP _) //. rewrite (sameP commgP cent1P); apply: subsetP (fZ y Gy). by rewrite subIset // orbC -cent_set1 centS // sub1set !(groupM, groupV). pose fm := Morphism fM. have fmG: fm @* G = 'Z(G). have sfmG: fm @* G \subset 'Z(G). by apply/subsetP=> _ /morphimP[z _ Gz ->]; apply: fZ. apply/eqP; rewrite eqEsubset sfmG; apply: contraR notZx => /(prime_TIg prZ). rewrite (setIidPr _) // => fmG1; rewrite inE Gx; apply/centP=> y Gy. by apply/commgP; rewrite -in_set1 -[[set _]]fmG1; apply: mem_morphim. have ->: 'C_G[x] = 'ker fm. apply/setP=> z; rewrite inE (sameP cent1P commgP) !inE. by rewrite -invg_comm eq_invg_mul mulg1. rewrite p_index_maximal ?subsetIl // -card_quotient ?ker_norm //. by rewrite (card_isog (first_isog fm)) /= fmG. 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)