proposition: Lemma acts_irr_mod G M : H \subset 'C(M | to) -> G \subset 'N(H) -> acts_irreducibly G M to -> acts_irreducibly (G / H) M mod_groupAction.
proof: Proof. move=> cMH nHG /mingroupP[/andP[ntM nMG] minM]. apply/mingroupP; rewrite ntM astabs_mod ?quotientS //; split=> // L modL ntL. have cLH: H \subset 'C(L | to) by rewrite (subset_trans cMH) ?astabS //. apply: minM => //; case/andP: modL => ->; rewrite astabs_mod ?quotientSGK //. by rewrite (subset_trans cLH) ?astab_sub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)