proposition: Lemma qacts_cosetpre (H : {group rT}) (K' : {group coset_of H}) : H \subset D -> [acts A, on H | to] -> [acts qact_dom to H, on K' | to / H] -> [acts A, on coset H @*^-1 K' | to].
proof: Proof. move=> sHD aH aK'; apply/subsetP=> x Ax; move: (Ax) (subsetP aK'). rewrite -{1}(acts_qact_doms sHD aH) => qdx; move/(_ x qdx) => nx. rewrite !inE Ax; apply/subsetP=> y; case/morphpreP=> Ny /= K'Hy /[1!inE]. apply/morphpreP; split; first by rewrite acts_qact_dom_norm. by move/gastabsP: nx; move/(_ qdx (coset H y)); rewrite K'Hy qactE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)