proposition: Lemma Fcore_Hall : \pi(M`_\F).-Hall(M) M`_\F.
proof: Proof. rewrite Hall_pi // /Hall Fcore_sub coprime_pi' ?cardG_gt0 //=. apply/pnatP=> // p p_pr; apply: contraL => /= piMFp; rewrite -p'natE //. rewrite -partn_eq1 // -(eqn_pmul2l (part_gt0 p #|M`_\F|)) muln1. rewrite -partnM ?cardG_gt0 // Lagrange ?Fcore_sub //. rewrite -(card_Hall (nilpotent_pcore_Hall p Fcore_nil)) /=. by rewrite p_core_Fcore // (card_Hall (Fcore_pcore_Sylow piMFp)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14)