proposition: Lemma mmeasure_eq0 g : (mmeasure g == 0%N) = (g == 0).
proof: Proof. apply/idP/eqP=> [z_g|->]; last by rewrite mmeasure0. apply/malgP=> k; rewrite mcoeff0; apply/contraTeq: z_g. rewrite mcoeff_neq0 => kg; rewrite mmeasureE. by rewrite (big_fsetD1 k) //= -lt0n leq_max. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap