proposition: Theorem odd_abelian_gen_stable : X / C \subset 'O_p(G / C).
proof: Proof. case/exists_eqP: genX => gX defX. rewrite -defN sub_quotient_pre // -defX gen_subG. apply/bigcupsP=> A gX_A; have [_ pA nAP cAA] := and4P gX_A. have{gX_A} sAX: A \subset X by rewrite -defX sub_gen ?bigcup_sup. rewrite -sub_quotient_pre ?(subset_trans sAX nCX) //=. rewrite odd_p_stable ?normalM ?pcore_normal //. by rewrite /psubgroup pA defN (subset_trans sAX sXG). by apply/commG1P; rewrite (subset_trans _ cAA) // commg_subr. 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)