proposition: Lemma monalgEw (g : {malg G[K]}) (domg : {fset K}) : msupp g `<=` domg -> g = \sum_(k <- domg) << g@_k *g k >>.
proof: Proof. move/fsubsetP=> le_gd; apply/malgP=> k; have [/le_gd kg|k_notin_g] := msuppP. rewrite raddf_sum (big_fsetD1 k) //= mcoeffUU big1_fset ?addr0 // => k'. by rewrite in_fsetD1 mcoeffU; case: eqP. rewrite raddf_sum /= big1_fset // => k' _ _. by rewrite mcoeffU; case: eqP k_notin_g => // <- /mcoeff_outdom ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap