proposition: Lemma sumn_nth_le l n : size l <= n -> sumn l = \sum_(0 <= i < n) nth 0 l i.
proof: Proof. by rewrite -sumn_take => /take_oversize ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)