proposition: Lemma Aut_isomP : isom (Aut G) (Aut (f @* G)) (Aut_isom injf sGD).
proof: Proof. by apply/isomP; split; [apply: injm_Aut_isom | apply: im_Aut_isom]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)