proposition: Lemma eq_def_multiQ l : ('C[l]%:Q = (\sum_(0 <= i < size l) l`_i)`!%:Q / (\prod_(0 <= i < size l) (l`_i)`!)%N%:Q)%R.
proof: Proof. have dn0 : ((\prod_(i <- l) i `!)%N%:Q != 0)%R. rewrite pnatr_eq0 -lt0n prodn_gt0 // => i; exact: fact_gt0. rewrite -(big_nth 0 xpredT) -(big_nth 0 xpredT id). by rewrite -multi_prod_fact !PoszM !rmorphM /= mulfK. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp