proposition: Lemma qactEcond x a : x \in 'N(H) -> quotient_action (coset H x) a = coset H (if a \in qact_dom then to x a else x).
proof: Proof. move=> Nx; apply: val_inj; rewrite val_subact //= qact_subdomE. have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f. case nNa: (a \in _); rewrite // -(astabs_act _ nNa). rewrite !val_coset ?(acts_act acts_qact_dom nNa) //=. case/rcosetsP=> y Ny defHy; rewrite defHy; apply: rcoset_eqP. by rewrite rcoset_sym -defHy (imset_f (_^~_)) ?rcoset_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)