proposition: Lemma psupport1 : psupport (perm_one T) = set0.
proof: Proof. Proof using. by apply/setP => x; rewrite in_psupport inE perm1 eq_refl. 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