proposition: Lemma im_Aut_isom : Aut_isom injf sGD @* Aut G = Aut (f @* G).
proof: Proof. apply/eqP; rewrite eqEcard; apply/andP; split. by apply/subsetP=> _ /morphimP[a _ AutGa ->]; apply: Aut_Aut_isom. have inj_isom' := injm_Aut_isom (injm_invm injf) (morphimS _ sGD). rewrite card_injm ?injm_Aut_isom // -(card_injm inj_isom') ?subset_leq_card //. apply/subsetP=> a /morphimP[a' _ AutfGa' def_a]. by rewrite -(morphim_invm injf sGD) def_a Aut_Aut_isom. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)