proposition: Lemma imset_autE A : A \subset G -> aut @: A = f @* A.
proof: Proof. move=> sAG; rewrite /morphim (setIidPr sAG). by apply: eq_in_imset; apply: sub_in1 autE; apply/subsetP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)