proposition: Lemma mnmwgtU i : mnmwgt U_(i) = i.+1.
proof: Proof. rewrite mnmwgtE (bigD1 i) //= cmUU mul1n big1 ?addn0 //. by move=> j ne_ij; rewrite cmU eq_sym (negbTE ne_ij). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap