proposition: Lemma eq_def_multi1 (l : list nat) : 'C[l] * \prod_(0 <= i < size l) (l`_i)`! = (\sum_(0 <= i < size l) l`_i)`!.
proof: Proof. rewrite -(big_nth 0 xpredT) -(big_nth 0 xpredT id). exact: multi_prod_fact. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp