proposition: Lemma acts_irr_mod_astab G M : acts_irreducibly G M to -> acts_irreducibly (G / 'C_G(M | to)) M (mod_groupAction _).
proof: Proof. move=> irrG; have /andP[_ nMG] := mingroupp irrG. apply: acts_irr_mod irrG; first exact: subsetIr. by rewrite normsI ?normG // (subset_trans nMG) // astab_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)