proposition: Lemma qacts_coset (H K : {group rT}) : H \subset D -> [acts A, on K | to] -> [acts qact_dom to H, on (coset H) @* K | to / H].
proof: Proof. move=> sHD aK. apply/subsetP=> x qdx; rewrite inE qdx inE; apply/subsetP=> y. case/morphimP=> z Nz Kz /= e; rewrite e inE qactE // imset_f // inE. move/gactsP: aK; move/(_ x (subsetP (qact_dom_doms sHD) _ qdx) z); rewrite Kz. move->; move/acts_act: (acts_qact_dom to H); move/(_ x qdx z). by rewrite Nz andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)