proposition: Lemma msupp0 : msupp 0 = fset0 :> {fset K}.
proof: Proof. apply/fsetP=> k; rewrite in_fset0; apply/negbTE. by rewrite -mcoeff_eq0 mcoeff0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap