proposition: Lemma Aut_Aut_isom a : Aut_isom a \in Aut (f @* G).
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)