proposition: Lemma disjoint_psupports_of_decomp A B : disjoint_psupports A -> disjoint_psupports B -> \prod_(C in A) C = \prod_(C in B) C -> {in A & B, forall c1 c2, psupport c1 = psupport c2 -> c1 = c2}.
proof: Proof. Proof using. move=> HdisjA HdisjB /permP Heq c1 c2 Hc1 Hc2 /setP Hsupp. apply/permP => x. case: (boolP (x \in psupport c1)) => /[dup]; rewrite {1}Hsupp. - move => Hx1 Hx2; move/(_ x): Heq. by rewrite (prod_of_disjoint _ Hc1) ?(prod_of_disjoint _ Hc2). - by rewrite !in_psupport !negbK => /eqP -> /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