proposition: Lemma qact_is_groupAction : is_groupAction (R / H) (to / H).
proof: Proof. move=> a HDa /=; have Da := astabs_dom HDa. rewrite inE; apply/andP; split. apply/subsetP=> Hx /=; case: (cosetP Hx) => x Nx ->{Hx}. apply: contraR => R'Hx; rewrite actpermE qactE // gact_out //. by apply: contra R'Hx; apply: mem_morphim. apply/morphicP=> Hx Hy; rewrite !actpermE. case/morphimP=> x Nx Gx ->{Hx}; case/morphimP=> y Ny Gy ->{Hy}. by rewrite -morphM ?qactE ?groupM ?gactM // morphM ?acts_qact_dom_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)