proposition: Lemma psupport_disjointC s t : [disjoint psupport s & psupport t] -> commute s t.
proof: Proof. Proof using. move=> Hdisj; apply/permP => x; rewrite !permM. case: (boolP (x \in psupport s)) => [Hs |]. - have:= Hdisj; rewrite disjoints_subset => /subsetP H. have:= H x Hs; rewrite inE in_psupport negbK => /eqP ->. move: Hs; rewrite psupport_stable => /H. by rewrite inE in_psupport negbK => /eqP ->. - rewrite in_psupport negbK => /eqP Hs; rewrite Hs. case: (boolP (x \in psupport t)) => [Ht |]. + move: Ht; rewrite psupport_stable. move: Hdisj; rewrite -setI_eq0 setIC setI_eq0 disjoints_subset => /subsetP. by move=> H{}/H; rewrite inE in_psupport negbK => /eqP ->. + by rewrite in_psupport negbK => /eqP ->; rewrite Hs. 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