proposition: Lemma subcent1_extraspecial_maximal U x : U \subset G -> x \in G :\: 'C(U) -> maximal 'C_U[x] U.
proof: Proof. move=> sUG /setDP[Gx not_cUx]; apply/maxgroupP; split=> [|H ltHU sCxH]. by rewrite /proper subsetIl subsetI subxx sub_cent1. case/andP: ltHU => sHU not_sHU; have sHG := subset_trans sHU sUG. apply/eqP; rewrite eqEsubset sCxH subsetI sHU /= andbT. apply: contraR not_sHU => not_sHCx. have maxCx: maximal 'C_G[x] G. rewrite cent1_extraspecial_maximal //; apply: contra not_cUx. by rewrite inE Gx; apply: subsetP (centS sUG) _. have nsCx := p_maximal_normal pG maxCx. rewrite -(setIidPl sUG) -(mulg_normal_maximal nsCx maxCx sHG) ?subsetI ?sHG //. by rewrite -group_modr //= setIA (setIidPl sUG) mul_subG. 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)