proposition: Lemma acts_qact_dom : [acts qact_dom, on 'N(H) | to].
proof: Proof. apply/subsetP=> a nNa; rewrite !inE (astabs_dom nNa); apply/subsetP=> x Nx. have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f. rewrite inE -(astabs_act _ nNa) => /rcosetsP[y Ny defHy]. have: to x a \in H :* y by rewrite -defHy (imset_f (to^~a)) ?rcoset_refl. by apply: subsetP; rewrite mul_subG ?sub1set ?normG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)