proposition: Lemma astabs_quotient (G : {group rT}) : H <| G -> 'N(G / H | quotient_action) = 'N_qact_dom(G | to).
proof: Proof. move=> nsHG; have [_ nHG] := andP nsHG. apply/eqP; rewrite eqEsubset acts_quotient // andbT. apply/subsetP=> a nGa; have dHa := astabs_dom nGa; have [Da _]:= setIdP dHa. rewrite inE dHa 2!inE Da; apply/subsetP=> x Gx; have nHx := subsetP nHG x Gx. rewrite -(quotientGK nsHG) 2!inE (acts_act acts_qact_dom) ?nHx //= inE. by rewrite -qactE // (astabs_act _ nGa) mem_morphim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)