proposition: Proposition solvable_p_constrained : solvable G -> p.-constrained G.
proof: Proof. move=> solG P sylP; have [sPO pP _] := and3P sylP; pose K := 'O_p^'(G). have nKG: G \subset 'N(K) by rewrite normal_norm ?pcore_normal. have nKC: 'C_G(P) \subset 'N(K) by rewrite subIset ?nKG. rewrite -(quotientSGK nKC) //; last first. by rewrite /= -pseries1 (pseries_sub_catl [::_]). apply: subset_trans (quotient_subcent _ _ _) _; rewrite /= -/K. suffices ->: P / K = 'O_p(G / K). rewrite quotient_pseries2 -Fitting_eq_pcore ?trivg_pcore_quotient // -/K. by rewrite cent_sub_Fitting ?morphim_sol. apply/eqP; rewrite eqEcard -(part_pnat_id (pcore_pgroup _ _)). have sylPK: p.-Sylow('O_p(G / K)) (P / K). rewrite -quotient_pseries2 morphim_pHall //. exact: subset_trans (subset_trans sPO (pseries_sub _ _)) nKG. by rewrite -(card_Hall sylPK) leqnn -quotient_pseries2 quotientS. 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)