proposition: Lemma card_psupport_noteq1 s : #|psupport s| != 1%N.
proof: Proof. Proof using. apply/cards1P => [[x] Hsupp]. have: s x == x by rewrite -in_set1 -Hsupp -psupport_stable Hsupp inE. by move => /eqP; apply/eqP; rewrite -in_psupport Hsupp inE. 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