proposition: Lemma sum_bin_rec (n :nat) (f: nat -> nat): \sum_(i<n.+1) 'C(n.+1,i.+1) * (f i) = \sum_(i<n) 'C(n,i.+1) * (f i) + \sum_(i<n.+1) 'C(n,i) * (f i).
proof: Proof. transitivity (\sum_(i < n.+1) 'C(n, i.+1) * (f i) + \sum_(i < n.+1) 'C(n, i) * (f i)). rewrite - big_split; apply eq_bigr => // i _; rewrite binS mulnDl //. by rewrite big_ord_recr /= bin_small ?addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)