proposition: Lemma leq_sumn_in (sh : seq nat) i : i \in sh -> i <= sumn sh.
proof: Proof. elim: sh => [//| s0 sh IHsh]. rewrite inE /= => /orP[/eqP->|/IHsh]; first exact: leq_addr. move/leq_trans; apply; exact: leq_addl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)