proposition: Lemma norm_conjg_im x : x \in 'N(G) -> conjgm G x @* G = G.
proof: Proof. by rewrite morphimEdom; apply: normP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)