proposition: Lemma sumn_take_leq s k1 k2 : k1 <= k2 -> sumn (take k1 s) <= sumn (take k2 s).
proof: Proof. rewrite !sumn_take; move=> H. by rewrite (big_cat_nat _ _ _ _ H) //=; apply leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype