proposition: Lemma psupport_restr_perm_incl X s : psupport (restr_perm X s) \subset X.
proof: Proof. Proof using. apply/subsetP => x; rewrite in_psupport. by apply contraR => /out_perm -> //; apply: restr_perm_on. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp