proposition: Lemma C_0k k : C 0 k = 1.
proof: Proof. move: (C_multi 0 k). have -> : \prod_(0 <= i < k) (0 %/ a i)`! = 1. by apply: big1 => i _; rewrite div0n fact0. by rewrite mul1n fact0. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial