proposition: Lemma Fcore_dprod : \big[dprod/1]_(P | Sylow M (gval P) && (P <| M)) P = M`_\F.
proof: Proof. rewrite -[M`_\F]bigprodGE. apply/eqP/bigdprodYP=> P /andP[/SylowP[p p_pr sylP] nsPM]. have defP := normal_Hall_pcore sylP nsPM. have /dprodP[_ _ cFpFp' tiFpFp'] := nilpotent_pcoreC p (Fitting_nil M). have /dprodYP := dprodEY cFpFp' tiFpFp'; rewrite /= p_core_Fitting defP. apply: subset_trans; rewrite bigprodGE gen_subG. apply/bigcupsP=> Q => /andP[/andP[/SylowP[q _ sylQ] nsQM] neqQP]. have defQ := normal_Hall_pcore sylQ nsQM; rewrite -defQ -p_core_Fitting. apply: sub_pcore => q' /eqnP->; apply: contraNneq neqQP => eq_qp. by rewrite -val_eqE /= -defP -defQ eq_qp. 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)