proposition: Lemma qactJ H (Hy : coset_of H) x : 'Q%act Hy x = if x \in 'N(H) then Hy ^ coset H x else Hy.
proof: Proof. case: (cosetP Hy) => y Ny ->{Hy}. by rewrite qactEcond // dom_qactJ; case Nx: (x \in 'N(H)); rewrite ?morphJ. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)