proposition: Lemma sum_take r s F : F 0 = 0 -> \sum_(l <- take r s) F l = \sum_(0 <= i < r) F (nth 0 s i).
proof: Proof. move => F0; elim: r s => [|r IHr] s /=. by rewrite take0 /index_iota /= !big_nil. case: s => [{IHr}| s0 s] /=. by rewrite big_nil; apply/esym/big1 => i _; rewrite nth_default. by rewrite big_nat_recl //= big_cons -IHr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)