proposition: Lemma FTcore_facts : [/\ Hall G M`_\F, Hall G M`_\s & forall S, Sylow M`_\s S -> S :!=: 1%g -> 'N(S) \subset M].
proof: Proof. have hallMs := Msigma_Hall_G maxM; have [_ sMs _] := and3P hallMs. rewrite def_FTcore // (pHall_Hall hallMs). split=> // [|S /SylowP[p _ sylS] ntS]. have sMF_Ms:= Fcore_sub_Msigma maxM. apply: (@pHall_Hall _ \pi(M`_\F)); apply: (subHall_Hall hallMs). by move=> p /(piSg sMF_Ms)/(pnatPpi sMs). exact: pHall_subl (pcore_sub _ M) (Fcore_Hall M). have s_p: p \in \sigma(M). by rewrite (pnatPpi sMs) // -p_rank_gt0 -(rank_Sylow sylS) rank_gt0. by apply: (norm_sigma_Sylow s_p); apply: (subHall_Sylow (Msigma_Hall maxM)). 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)