proposition: Lemma conj_isom x : isom G (G :^ x) (conjgm G x).
proof: Proof. by apply/isomP; rewrite morphim_conj setIid injm_conj. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)