proposition: Lemma restr_perm_isom : isom (inH @* Aut G) (infH @* Aut (f @* G)) fHisom.
proof: Proof. apply: sub_isom; rewrite ?restr_perm_Aut ?injm_Aut_isom //=. rewrite -(im_Aut_isom injf sGD) -!morphim_comp. apply: eq_in_morphim; last exact: isom_restr_perm. apply/setP=> a; rewrite in_setI [in RHS]in_setI; apply: andb_id2r => AutGa. rewrite /= inE andbC inE (Aut_restr_perm sHG) //=. by symmetry; rewrite inE AutGa inE astabs_Aut_isom. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)