proposition: Lemma preim_autE A : A \subset G -> aut @^-1: A = f @*^-1 A.
proof: Proof. move=> sAG; apply/setP=> x; rewrite !inE permE /=. by case Gx: (x \in G) => //; apply/negP=> Ax; rewrite (subsetP sAG) in Gx. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)