proposition: Theorem Malpha_Hall : \alpha(M).-Hall(M) M`_\alpha.
proof: Proof. have [H hallH] := Hall_exists \sigma(M) solM; have [sHM sH _] := and3P hallH. rewrite (subHall_Hall hallH (alpha_sub_sigma maxM)) // /pHall pcore_pgroup /=. rewrite -(card_quotient (subset_trans sHM (normal_norm nsMaM))) -pgroupE. rewrite (subset_trans sMaMs) ?pcore_sub_Hall ?(pgroupS _ alpha'F) //=. exact: subset_trans (quotientS _ (sigma_Hall_sub_der1 hallH)) _. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)