proposition: Lemma im_autm : f @* G = G.
proof: Proof. apply/setP=> x; rewrite morphimEdom (can_imset_pre _ (permK a)) inE. by have /[1!inE] /andP[/perm_closed <-] := AutGa; rewrite permKV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)