proposition: Lemma mnmwgt_eq0I m : mnmwgt m = 0%N -> m = 1%M.
proof: Proof. move=> h; apply/eqP/cmP=> /= i; move: h; rewrite mnmwgtE cm1 => /eqP. rewrite sum_nat_eq0 => /forallP /(_ i) /implyP. by rewrite muln_eq0 orbF => z_mi; apply/eqP/z_mi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap