proposition: Lemma sumn_drop r s : sumn (drop r s) = \sum_(r <= i < size s) nth 0 s i.
proof: Proof. case: (ltnP r (size s)) => [/ltnW ltrsz | leszr]; first last. by rewrite drop_oversize // big_geq. rewrite sumnE (big_nth 0) size_drop -{3}(add0n r) big_addn. by apply eq_bigr => i _; rewrite nth_drop addnC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)