proposition: Lemma qact_domE : H \subset R -> qact_dom to H = 'N(H | to).
proof: Proof. move=> sHR; apply/setP=> a; apply/idP/idP=> nHa; have Da := astabs_dom nHa. rewrite !inE Da; apply/subsetP=> x Hx; rewrite inE -(rcoset1 H). have /rcosetsP[y Ny defHy]: to^~ a @: H \in rcosets H 'N(H). by rewrite (astabs_act _ nHa); apply/rcosetsP; exists 1; rewrite ?mulg1. by rewrite (rcoset_eqP (_ : 1 \in H :* y)) -defHy -1?(gact1 Da) mem_setact. rewrite !inE Da; apply/subsetP=> Hx /[1!inE] /rcosetsP[x Nx ->{Hx}]. apply/imsetP; exists (to x a). case Rx: (x \in R); last by rewrite gact_out ?Rx. rewrite inE; apply/subsetP=> _ /imsetP[y Hy ->]. rewrite -(actKVin to Da y) -gactJ // ?(subsetP sHR, astabs_act, groupV) //. by rewrite memJ_norm // astabs_act ?groupV. apply/eqP; rewrite rcosetE eqEcard. rewrite (card_imset _ (act_inj _ _)) !card_rcoset leqnn andbT. apply/subsetP=> _ /imsetP[y Hxy ->]; rewrite !mem_rcoset in Hxy *. have Rxy := subsetP sHR _ Hxy; rewrite -(mulgKV x y). case Rx: (x \in R); last by rewrite !gact_out ?mulgK // 1?groupMl ?Rx. by rewrite -gactV // -gactM 1?groupMr ?groupV // mulgK astabs_act. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)