proposition: Lemma mfE m : mf m = (\sum_(i < n) (m i) * mf U_(i)%MM)%N.
proof: Proof. rewrite {1}(multinomUE_id m) (big_morph mf mfD mf0); apply/eq_bigr => i _. elim: (m i) => [// | d ih] /=; first by rewrite mul0n mulm0n mf0. by rewrite mulmS mulSn mfD ih. 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