proposition: Lemma msupp_eq0 (g : {malg G[K]}) : (msupp g == fset0) = (g == 0).
proof: Proof. apply/eqP/eqP=> [/fsetP z_g|->]; last exact: msupp0. by apply/malgP=> i; rewrite mcoeff0 mcoeff_outdom // z_g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap