proposition: Lemma msuppB g1 g2 : [disjoint msupp g1 & msupp g2] -> msupp (g1 - g2) = msupp g1 `|` msupp g2.
proof: Proof. by move=> dj_g1g2; rewrite msuppD msuppN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap