proposition: Lemma psupport_expg s n : psupport (s ^+ n) \subset psupport s.
proof: Proof. Proof using. by apply/subsetP => x; rewrite !in_psupport; apply contra => /eqP/permX_fix ->. 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