proposition: Lemma msuppZ c g : msupp (c *: g) = if c == 0 then fset0 else msupp g.
proof: Proof. case: eqP=> [->|/eqP nz_c]; first by rewrite scale0r msupp0. by apply/fsetP=> k; rewrite -!mcoeff_neq0 mcoeffZ mulf_eq0 negb_or nz_c. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap