proposition: Lemma msuppU k x : msupp << x *g k >> = if x == 0 then fset0 else [fset k].
proof: Proof. apply/fsetP=> k'; rewrite -mcoeff_neq0 mcoeffU 2!fun_if !inE. by have [//|_] := eqVneq k k'; rewrite eqxx if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap