proposition: Lemma typeII_IV_core (p := #|W2|) : if FTtype M == 2 then 'C_H(U) = 1 /\ #|H| = (#|W2| ^ q)%N else [/\ prime p, 'C_H(U <*> W1) = 1 & #|H| = (p ^ q * #|'C_H(U)|)%N].
proof: Proof. have [_ _ nHUW1 _] := sdprodP defHUW1. have /= [oH _ oH1] := Frobenius_Wielandt_fixpoint frobUW1 nHUW1 coH_UW1 solH. have [Mtype2 {oH}| notMtype2 {oH1}] := boolP (FTtype M == 2). suffices regHU: 'C_H(U) = 1 by rewrite -defW2 oH1. have [_ _ _ HUtypeF defHUF] := compl_of_typeII maxM MtypeP Mtype2. have [_ _ [U0 [sU0U _]]] := HUtypeF; rewrite {}defHUF => frobHU0. have /set0Pn[x U0x]: U0^# != set0. by rewrite setD_eq0 subG1; case/Frobenius_context: frobHU0. apply/trivgP; rewrite -(Frobenius_reg_ker frobHU0 U0x) setIS // -cent_cycle. by rewrite centS // cycle_subG (subsetP sU0U) //; case/setD1P: U0x. have p_pr: prime p. have [S pairMS [xdefW [U_S StypeP]]] := FTtypeP_pair_witness maxM MtypeP. have [[_ _ maxS] _] := pairMS; rewrite {1}(negPf notMtype2) /= => Stype2 _ _. by have [[]] := compl_of_typeII maxS StypeP Stype2. rewrite -/q -/p centY setICA defW2 setIC in oH *. suffices regW2U: 'C_W2(U) = 1 by rewrite -oH regW2U cards1 exp1n mul1n. apply: prime_TIg => //=; apply: contra not_cHU => /setIidPl cUW2. rewrite centsC (sameP setIidPl eqP) eqEcard subsetIl. by rewrite -(@leq_pmul2l (p ^ q)) -?oH ?cUW2 //= expn_gt0 cardG_gt0. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator center gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection8)