proposition: Theorem FTtype1_Frobenius M : M \in 'M -> FTtype M == 1%N -> [Frobenius M with kernel M`_\F].
proof: Proof. set K := M`_\F => maxM Mtype1; have [U [MtypeF _]] := FTtypeP 1 maxM Mtype1. have hallU: \pi(K)^'.-Hall(M) U. by rewrite -(compl_pHall U (Fcore_Hall M)) sdprod_compl; have [[]] := MtypeF. apply: FrobeniusWker (U) _ _; have{MtypeF} [_ -> _] := typeF_context MtypeF. apply/forall_inP=> P /SylowP[p _ sylP]. rewrite (odd_pgroup_rank1_cyclic (pHall_pgroup sylP)) ?mFT_odd // leqNgt. apply/negP=> prankP. have piUp: p \in \pi(U) by rewrite -p_rank_gt0 -(p_rank_Sylow sylP) ltnW. have{piUp} K'p: p \in \pi(K)^' := pnatPpi (pHall_pgroup hallU) piUp. have{U hallU} sylP: p.-Sylow(M) P := subHall_Sylow hallU K'p sylP. have{P sylP prankP} prankM: (1 < 'r_p(M))%N by rewrite -(p_rank_Sylow sylP). case/negP: K'p => /=; move: {2}p.+1 (ltnSn p) => n ltpn. elim: n => // n IHn in p M @K ltpn maxM Mtype1 prankM *. move: ltpn; rewrite ltnS leq_eqVlt => /predU1P[Dp | /IHn-> //]. apply/idPn=> p'K; rewrite -p'groupEpi /= -/K -{n}Dp in p'K IHn. have [P sylP] := Sylow_exists p M. case/non_Frobenius_FTtype1_witness: (sylP) => // cPP prankP [L [maxL sPLs]]. by case=> x P1s_x []; apply: (FTtype1_nonFrobenius_contradiction IHn) P1s_x. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)