proposition: Lemma plength1_Sylow_Jsub (Q : {group gT}) : Q \subset G -> p.-group Q -> exists2 x, x \in 'C_G(Q :&: S) & Q :^ x \subset S.
proof: Proof. move=> sQG pQ; have sQ_Gp'p: Q \subset 'O_{p^',p}(G). rewrite -sub_quotient_pre /= pcore_mod1 ?(subset_trans sQG) //. by rewrite (sub_Hall_pcore sylGbp) ?quotientS ?quotient_pgroup. have [xy /= KSxy sQxyS] := Sylow_Jsub sylS_Gp'p sQ_Gp'p pQ. rewrite -plength1_Sylow_prod in KSxy; have [x y Kx Sy def_xy] := mulsgP KSxy. have{sQxyS} sQxS: Q :^ x \subset S. by rewrite -(conjSg _ _ y) (conjGid Sy) -conjsgM -def_xy. exists x; rewrite // inE (subsetP sKG) //; apply/centP=> z; case/setIP=> Qz Sz. apply/commgP; rewrite -in_set1 -set1gE -(coprime_TIg coKS) inE. rewrite groupMl ?groupV ?memJ_norm ?(subsetP nKS) ?Kx //=. by rewrite commgEr groupMr // (subsetP sQxS) ?memJ_conjg ?groupV. 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)