proposition: Lemma Aut_restr_perm a : a \in Aut G -> restr_perm H a \in Aut H.
proof: Proof. move=> AutGa. case nHa: (a \in 'N(H | 'P)); last by rewrite triv_restr_perm ?nHa ?group1. rewrite inE restr_perm_on; apply/morphicP=> x y Hx Hy /=. by rewrite !restr_permE ?groupM // -(autmE AutGa) morphM ?(subsetP sHG). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)