proposition: Lemma multi_prod_fact l : 'C[l] * \prod_(j <- l) j`! = (\sum_(j <- l) j)`!.
proof: Proof. elim/last_ind: l => [| l n ihl]; first by rewrite multi_nil !big_nil. set p := \prod_(_ <- _) _; set s := \sum_(_ <- _) _. rewrite multi_rcons mulnAC. have aux : (rcons l n)`_(size l) = n by rewrite nth_rcons ltnn eqxx. have -> : p = \prod_(j <- l) j`! * n`! by rewrite /p -cats1 big_cat /= big_seq1. rewrite mulnA ihl. have es : s = \sum_(j <- l) j + n by rewrite /s -cats1 big_cat /= big_seq1. rewrite -es mulnC [X in _ * X = _]mulnC. have -> : \sum_(j <- l) j = s - n by rewrite es addnK. by rewrite bin_fact // es leq_addl. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp