proposition: Lemma qactE x a : x \in 'N(H) -> a \in qact_dom -> quotient_action (coset H x) a = coset H (to x a).
proof: Proof. by move=> Nx nNa; rewrite qactEcond ?nNa. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)