proposition: Lemma part_sumn_rectangle sh : is_part sh -> sumn sh <= (head 0 sh) * (size sh).
proof: Proof. elim: sh => //= s0 s IHs /andP[Hhead {}/IHs Hsum]. rewrite mulnS leq_add2l; apply (leq_trans Hsum) => {Hsum}; rewrite leq_mul2r. by case: s Hhead. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype