proposition: Lemma psupport_perm_on S s : (perm_on S s) = (psupport s \subset S).
proof: Proof. Proof using. apply/subsetP/subsetP => H x. - rewrite in_psupport; exact: H. - rewrite inE -in_psupport; exact: H. 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