proposition: Lemma Aut_in_isog : Aut_in (Aut G) H \isog restr_perm H @* Aut G.
proof: Proof. rewrite /Aut_in -ker_restr_perm kerE -morphpreIdom -morphimIdom -kerE /=. by rewrite setIA (setIC _ (Aut G)) first_isog_loc ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)