proposition: Lemma Aut_isomE a : a \in Aut G -> {in G, forall x, Aut_isom a (f x) = f (a x)}.
proof: Proof. by rewrite /Aut_isom; case: (Aut_isom_subproof a). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)