proposition: Theorem Burnside_normal_complement : 'N_G(S) \subset 'C(S) -> 'O_p^'(G) ><| S = G.
proof: Proof. move=> cSN; set K := 'O_p^'(G); have [sSG pS _] := and3P sylS. have /andP[sKG nKG]: K <| G by apply: pcore_normal. have{nKG} nKS := subset_trans sSG nKG. have p'K: p^'.-group K by apply: pcore_pgroup. have{pS p'K} tiKS: K :&: S = 1 by rewrite setIC coprime_TIg ?(pnat_coprime pS). suffices{tiKS nKS} hallK: p^'.-Hall(G) K. rewrite sdprodE //= -/K; apply/eqP; rewrite eqEcard ?mul_subG //=. by rewrite TI_cardMg //= (card_Hall sylS) (card_Hall hallK) mulnC partnC. pose G' := G^`(1); have nsG'G : G' <| G by rewrite der_normalS. suffices{K sKG} p'G': p^'.-group G'. have nsG'K: G' <| K by rewrite (normalS _ sKG) ?pcore_max. rewrite -(pquotient_pHall p'G') -?pquotient_pcore //= -/G'. by rewrite nilpotent_pcore_Hall ?abelian_nil ?der_abelian. suffices{nsG'G} tiSG': S :&: G' = 1. have sylG'S : p.-Sylow(G') (G' :&: S) by rewrite (Sylow_setI_normal _ sylS). rewrite /pgroup -[#|_|](partnC p) ?cardG_gt0 // -{sylG'S}(card_Hall sylG'S). by rewrite /= setIC tiSG' cards1 mul1n part_pnat. apply/trivgP; rewrite /= focal_subgroup_gen ?(p_Sylow sylS) // gen_subG. apply/subsetP=> _ /imset2P[x u Sx /setIdP[Gu Sxu] ->]. have cSS y: y \in S -> S \subset 'C_G[y]. rewrite subsetI sSG -cent_set1 centsC sub1set; apply: subsetP. by apply: subset_trans cSN; rewrite subsetI sSG normG. have{cSS} [v]: exists2 v, v \in 'C_G[x ^ u | 'J] & S :=: (S :^ u) :^ v. have sylSu : p.-Sylow(G) (S :^ u) by rewrite pHallJ. have [sSC sCG] := (cSS _ Sxu, subsetIl G 'C[x ^ u]). rewrite astab1J; apply: (@Sylow_trans p); apply: pHall_subl sCG _ => //=. by rewrite -conjg_set1 normJ -(conjGid Gu) -conjIg conjSg cSS. rewrite in_set1 -conjsgM => /setIP[Gv /astab1P cx_uv] nSuv. apply/conjg_fixP; rewrite -cx_uv /= -conjgM; apply: astabP Sx. by rewrite astabJ (subsetP cSN) // !inE -nSuv groupM /=. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)