proposition: Theorem Puig_center_p'core_normal p G S : odd #|G| -> solvable G -> p.-Sylow(G) S -> 'O_p^'(G) * 'Z('L(S)) <| G.
proof: Proof. move=> oddG solG sylS; rewrite -{2}(Puig_factorisation _ _ sylS) //. have sZL_G: 'Z('L(S)) \subset G by rewrite !gFsub_trans ?(pHall_sub sylS). rewrite -!quotientK ?(subset_trans sZL_G) ?subIset ?gFnorm //=. by rewrite cosetpre_normal quotient_normal // normalSG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)