proposition: Lemma sumn_included inner outer : included inner outer -> sumn inner <= sumn outer.
proof: Proof. elim: inner outer => [// | inn0 inn IHinn] /=. case=> [// | outer0 outer] /= /andP[H0 /IHinn]. exact: leq_add. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype