proposition: Lemma acts_irrQ G U V : G \subset 'N(V) -> V <| U -> acts_irreducibly G (U / V) 'Q = minnormal (U / V) (G / V).
proof: Proof. move=> nVG nsVU; apply/mingroupP/mingroupP; case=> /andP[->] /=. rewrite astabsQ // subsetI nVG /= => nUG minUV. rewrite quotient_norms //; split=> // H /andP[ntH nHG] sHU. by apply: minUV (sHU); rewrite ntH -(cosetpreK H) actsQ // norm_quotient_pre. rewrite sub_quotient_pre // => nUG minU; rewrite astabsQ //. rewrite (subset_trans nUG); last first. by rewrite subsetI subsetIl /= -{2}(quotientGK nsVU) morphpre_norm. split=> // H /andP[ntH nHG] sHU. rewrite -{1}(cosetpreK H) astabsQ ?normal_cosetpre ?subsetI ?nVG //= in nHG. apply: minU sHU; rewrite ntH; apply: subset_trans (quotientS _ nHG) _. by rewrite -{2}(cosetpreK H) quotient_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)