proposition: Lemma fgmulUg c k g : fgmul << c *g k >> g = \sum_(k' <- msupp g) << c * g@_k' *g k * k' >>.
proof: Proof. rewrite (fgmullw msuppU_le (fsubset_refl _)) 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