proposition: Lemma multi_rcons n l : 'C[rcons l n] = 'C[l] * 'C(\sum_(j <- l) j + n, n).
proof: Proof. rewrite [in LHS]/multinomial [in RHS](big_nth 0) size_rcons !big_nat_recr //=. have -> : (rcons l n)`_(size l) = n by rewrite nth_rcons ltnn eqxx. have aux k : 0 <= k < size l -> (rcons l n)`_k = l`_k. by rewrite nth_rcons; case/andP=> _ ->. rewrite !big_nat (eq_bigr _ aux) -big_nat; congr (_ * _); rewrite /multinomial. rewrite !big_nat; apply: eq_bigr => i ?; rewrite aux // !big_nat; congr 'C(_, _). by apply: eq_bigr=> j /andP[le0j leji]; rewrite aux // le0j (leq_trans leji). Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp