proposition: Lemma sdprod_sigma : M`_\sigma ><| E = M.
proof: Proof. rewrite sdprodE ?coprime_TIg ?(subset_trans sEM) ?gFnorm //. apply/eqP; rewrite eqEcard mul_subG ?pcore_sub ?coprime_cardMg //=. by rewrite (card_Hall (Msigma_Hall maxM)) (card_Hall hallE) partnC. 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 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)