proposition: Lemma typePF_exclusion K : ~ of_typeF M K.
proof: Proof. move=> [[ntH ntU1 defM_K] _ [U0 [sU01 expU0] frobU0]]. have [[cycW1 hallW1 ntW1 defM] [_ _ _ defM'] _ [_]] := MtypeP; case/negP. pose p := pdiv #|W1|; rewrite -/M' -/H in defM defM' frobU0 *. have piW1p: p \in \pi(W1) by rewrite pi_pdiv cardG_gt1. have piU0p: p \in \pi(U0). rewrite -pi_of_exponent expU0 pi_of_exponent (pi_of_dvd _ _ piW1p) //=. rewrite -(@dvdn_pmul2l #|H|) ?cardG_gt0 // (sdprod_card defM_K). rewrite -(sdprod_card defM) dvdn_pmul2r ?cardSg //. by case/sdprodP: defM' => _ <- _ _; apply: mulG_subl. have [|X EpX]:= @p_rank_geP _ p 1 U0 _; first by rewrite p_rank_gt0. have [ntX [sXU0 abelX _]] := (nt_pnElem EpX isT, pnElemP EpX). have piW1_X: \pi(W1).-group X by apply: pi_pgroup piW1p; case/andP: abelX. have sXM: X \subset M. by rewrite -(sdprodWY defM_K) joingC sub_gen ?subsetU // (subset_trans sXU0). have nHM: M \subset 'N(H) by apply: gFnorm. have [regU0 solM] := (Frobenius_reg_ker frobU0, of_typeP_sol). have [a Ma sXaW1] := Hall_Jsub solM (Hall_pi hallW1) sXM piW1_X. rewrite -subG1 -(conjs1g a) -(cent_semiregular regU0 sXU0 ntX) conjIg -centJ. by rewrite (normsP nHM) // -typeP_cent_core_compl ?setIS ?centS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)