proposition: Theorem odd_abelian_gen_constrained : 'O_p^'(G) = 1 -> 'C_('O_p(G))(P) \subset P -> X \subset 'O_p(G).
proof: Proof. set Q := 'O_p(G) => p'G1 sCQ_P. have sPQ: P \subset Q by rewrite pcore_max. have defQ: 'O_{p^', p}(G) = Q by rewrite pseries_pop2. have pQ: p.-group Q by apply: pcore_pgroup. have sCQ: 'C_G(Q) \subset Q. by rewrite -{2}defQ solvable_p_constrained //= defQ /pHall pQ indexgg subxx. have pC: p.-group C. apply/pgroupP=> q q_pr; case/Cauchy=> // u Cu q_u; apply/idPn=> p'q. suff cQu: u \in 'C_G(Q). case/negP: p'q; have{q_u}: q %| #[u] by rewrite q_u. by apply: pnatP q q_pr => //; apply: mem_p_elt pQ _; apply: (subsetP sCQ). have [Gu cPu] := setIP Cu; rewrite inE Gu /= -cycle_subG. rewrite coprime_nil_faithful_cent_stab ?(pgroup_nil pQ) //= -/C -/Q. - by rewrite cycle_subG; apply: subsetP Gu; rewrite normal_norm ?pcore_normal. - by rewrite (pnat_coprime pQ) // [#|_|]q_u pnatE. have sPcQu: P \subset 'C_Q(<[u]>) by rewrite subsetI sPQ centsC cycle_subG. by apply: subset_trans (subset_trans sCQ_P sPcQu); rewrite setIS // centS. rewrite -(quotientSGK nCX) ?pcore_max // -pquotient_pcore //. exact: odd_abelian_gen_stable. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop prime finset ssralg fingroup morphism) mathcomp(automorphism quotient gfunctor commutator zmodp center pgroup) mathcomp(sylow gseries nilpotent abelian maximal) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)