proposition: Lemma im_restr_perm p : restr_perm p @: S = S.
proof: Proof. exact: im_perm_on (restr_perm_on p). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)