proposition: Lemma pcore_sub_astab_irr G M : p.-group M -> M \subset R -> acts_irreducibly G M to -> 'O_p(G) \subset 'C_G(M | to).
proof: Proof. move=> pM sMR /mingroupP[/andP[ntM nMG] minM]. have /andP[sGpG nGpG]: 'O_p(G) <| G := gFnormal _ G. have sGD := acts_dom nMG; have sGpD: 'O_p(G) \subset D := gFsub_trans _ sGD. rewrite subsetI sGpG -gacentC //=; apply/setIidPl; apply: minM (subsetIl _ _). rewrite nontrivial_gacent_pgroup ?pcore_pgroup //=; last first. by split; rewrite ?gFsub_trans. by apply: subset_trans (acts_subnorm_subgacent sGpD nMG); rewrite subsetI subxx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)