proposition: Lemma F23 n m: \sum_(i<m) 'C(n+i, n) = 'C(n+m, n.+1).
proof: Proof. elim: m; first by rewrite big_ord0 bin_small // addn0 //. by move => m Hrec;rewrite big_ord_recr /= Hrec - binS addnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)