proposition: Lemma acts_qact_dom_norm : {acts qact_dom to H, on 'N(H) | to}.
proof: Proof. move=> a HDa /= x; rewrite {2}(('N(H) =P to^~ a @^-1: 'N(H)) _) ?inE {x}//. rewrite eqEcard (card_preimset _ (act_inj _ _)) leqnn andbT. apply/subsetP=> x Nx; rewrite inE; move/(astabs_act (H :* x)): HDa. rewrite mem_rcosets mulSGid ?normG // Nx => /rcosetsP[y Ny defHy]. suffices: to x a \in H :* y by apply: subsetP; rewrite mul_subG ?sub1set ?normG. by rewrite -defHy; apply: imset_f; apply: rcoset_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)