proposition: Lemma size_part sh : is_part sh -> size sh <= sumn sh.
proof: Proof. elim: sh => //= s0 sh IHsh /andP[Hhead Hpart]. apply: (leq_ltn_trans (IHsh Hpart)). rewrite -{1}[sumn sh]add0n ltn_add2r. have /part_head_non0 /= : is_part (s0 :: sh) by rewrite /= Hhead Hpart. by rewrite lt0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype