proposition: Lemma mnmwiden1 i : (mnmwiden U_(i) = U_(widen i))%MM.
proof: Proof. apply/mnmP; case=> j /= lt; rewrite /mnmwiden !mnmE; apply/esym. rewrite eqE multinomE /tnth /=; move: (tnth_default _ _) => x. rewrite nth_rcons size_map size_enum_ord; move: lt. rewrite ltnS leq_eqVlt => /predU1P[->|lt]. by apply/eqP; rewrite ltnn eqxx eqb0 ltn_eqF. rewrite lt (nth_map i) ?size_enum_ord //. by apply/esym; rewrite eqE /= nth_enum_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg