fact: Definition disjoint_psupports A := trivIset [set psupport C| C in A] /\ {in A &, injective psupport}.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp