proposition: Lemma multinomUE_id n (m : 'X_{1..n}) : m = (\sum_i U_(i) *+ m i)%MM.
proof: Proof. apply/mnmP=> i; rewrite mnm_sumE (bigD1 i) //=. rewrite big1; first by rewrite addn0 mulmnE mnm1E eqxx mul1n. by move=> j ne_ji; rewrite mulmnE mnm1E (negbTE ne_ji). 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