proposition: Lemma restr_perm_on p : perm_on S (restr_perm p).
proof: Proof. apply/subsetP=> x; apply: contraR => notSx. by rewrite permE /= /actby (negPf notSx). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)