proposition: Lemma psupport_eq0 s : (s == 1) = (psupport s == set0).
proof: Proof. Proof using. apply/eqP/eqP => [ -> |]; first exact: psupport1. move/setP => Heq; rewrite -permP => x. by move/(_ x): Heq; rewrite in_psupport inE perm1 => /eqP. 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