proposition: Lemma norm_conj_isom x : x \in 'N(G) -> isom G G (conjgm G x).
proof: Proof. by move/norm_conjg_im/restr_isom_to/(_ (conj_isom x))->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)