proposition: Lemma acts_quotient (A : {set aT}) (B : {set rT}) : A \subset 'N_qact_dom(B | to) -> [acts A, on B / H | quotient_action].
proof: Proof. move=> nBA; apply: subset_trans {A}nBA _; apply/subsetP=> a /setIP[dHa nBa]. rewrite inE dHa inE; apply/subsetP=> _ /morphimP[x nHx Bx ->]. rewrite inE /= qactE //. by rewrite mem_morphim ?(acts_act acts_qact_dom) ?(astabs_act _ nBa). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)