proposition: Lemma msuppD g1 g2 : [disjoint msupp g1 & msupp g2] -> msupp (g1 + g2) = msupp g1 `|` msupp g2.
proof: Proof. move=> dj_g1g2; apply/fsetP=> k; move/fdisjointP/(_ k): dj_g1g2. rewrite in_fsetU -!mcoeff_neq0 mcoeffD negbK. have [->|] //= := eqVneq (g1@_k) 0; first by rewrite add0r. by move=> + /(_ isT) /eqP ->; rewrite addr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap