proposition: Lemma psupport_of_disjoint A : disjoint_psupports A -> psupport (\prod_(C0 in A) C0) = \bigcup_(C0 in A) psupport C0.
proof: Proof. Proof using. move=> Hdisj; apply/setP => x. rewrite in_psupport; apply/idP/bigcupP => [H | [C] HC Hx]. - apply/exists_inP. apply/contraR: H; rewrite negb_exists_in => /forallP Hsupp. apply/eqP; apply out_perm_prod => C. by move/implyP: (Hsupp C). - by rewrite (prod_of_disjoint Hdisj HC Hx) -in_psupport. 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