proposition: Remark normed_constrained_Hall : pi^'.-Hall('C(A)) K.
proof: Proof. have [_ ntA prA _] := cstrA; rewrite -[setT]/G in prA. rewrite /pHall pcore_pgroup pcore_sub pnatNK /=. rewrite -card_quotient ?gFnorm //= -/K. apply/pgroupP=> p p_pr; case/Cauchy=> // Kx; case/morphimP=> x Nx Cx ->{Kx}. rewrite /order -quotient_cycle //= -/K => def_p; apply/idPn=> pi'p. have [P sylP] := Sylow_exists p <[x]>; have [sPx pP _]:= and3P sylP. suffices: P \subset K. have nKP: P \subset 'N(K) by rewrite (subset_trans sPx) ?cycle_subG. rewrite -quotient_sub1 //= -/K (sameP trivgP eqP) trivg_card1. rewrite (card_Hall (morphim_pHall _ nKP sylP)) def_p part_pnat_id ?pnat_id //. by case: eqP p_pr => // ->. suffices sP_pAC: P \subset 'O_pi^'(A <*> 'C(A)). rewrite (subset_trans sP_pAC) ?pcore_max ?pcore_pgroup //. rewrite /normal gFnorm_trans ?normsG ?joing_subr // andbT. rewrite -quotient_sub1; last first. by rewrite gFsub_trans // join_subG !(normG, norms_cent). rewrite /= -(setIidPr (pcore_sub _ _)) quotientGI ?joing_subr //=. rewrite {1}cent_joinEr // quotientMidr coprime_TIg // coprime_morph //. by rewrite coprime_pi' ?cardG_gt0 //= -/pi [pnat _ _]pcore_pgroup. apply: hyp71; first exact: joing_subl. apply: sub_proper_trans (mFT_norm_proper ntA prA). by rewrite join_subG normG cent_sub. have sPC: P \subset 'C(A) by rewrite (subset_trans sPx) ?cycle_subG. rewrite inE /psubgroup cents_norm 1?centsC // andbT. rewrite (subset_trans sPC) ?joing_subr //=. by apply: sub_in_pnat pP => p' _; move/eqnP->. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)