proposition: Lemma restr_permE : {in 'N(S | 'P) & S, forall p, restr_perm p =1 p}.
proof: Proof. by move=> y x nSp Sx; rewrite /= actpermE actbyE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)