proposition: Lemma nth_C_row n k i : nth 0 (C_row n k) i = if i < k then n %/ a i else if i == k then n - \sum_(0 <= i < k) n %/ a i else 0.
proof: Proof. by rewrite /C_row nth_rcons size_mkseq; case: ifP=> // ltik; rewrite nth_mkseq. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial