proposition: Lemma conj_aut_morphM : {in 'N(G) &, {morph conj_aut : x y / x * y}}.
proof: Proof. move=> x y nGx nGy; apply/permP=> z /=; rewrite permM. case Gz: (z \in G); last by rewrite !permE /= !Gz. by rewrite !norm_conj_autE // (conjgM, memJ_norm, groupM). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)