proposition: Lemma fgmulgU c k g : fgmul g << c *g k >> = \sum_(k' <- msupp g) << g@_k' * c *g k' * k >>.
proof: Proof. rewrite (fgmulrw (fsubset_refl _) msuppU_le) big_seq_fset1. by apply/eq_bigr=> k' _; rewrite mcoeffUU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap