proposition: Lemma C_multi n k : \prod_(0 <= i < k) (n %/ a i)`! * C n k = n`!.
proof: Proof. rewrite /C -mulnCA; set l := C_row n k; set p := (X in _ * X = _). suff [-> ->] : n = (\sum_(0 <= i < size l) nth 0 l i) /\ p = \prod_(0 <= i < size l) (nth 0 l i)`! by exact: eq_def_multi1. have nth_l i : 0 <= i < k -> (n %/ a i) = nth 0 (C_row n k) i. by case/andP => [_ ltik]; rewrite nth_C_row ltik. have {p} -> : p = \prod_(0 <= i < size l) (nth 0 l i)`!. rewrite /l size_C_row big_nat_recr //= nth_C_row ltnn eqxx; congr (_ * _). by apply: eq_big_nat => ? ?; rewrite nth_l. suff -> : n = \sum_(0 <= i < size l) nth 0 l i by []. rewrite /l size_C_row big_nat_recr //= nth_C_row ltnn eqxx. have -> : \sum_(0 <= i < k) nth 0 (C_row n k) i = \sum_(0 <= i < k) n %/ a i. by apply: eq_big_nat => ? ?; rewrite nth_l. rewrite subnKC //; exact: sum_aV_leqn. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial