proposition: Lemma sumn_take r s : sumn (take r s) = \sum_(0 <= i < r) nth 0 s i.
proof: Proof. by rewrite sumnE sum_take. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)