proposition: Lemma Aut_closed x : x \in G -> a x \in G.
proof: Proof. by move=> Gx; rewrite -im_autm; apply: mem_morphim. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)