proposition: Lemma intpartn_nth0 d (la : 'P_d) : nth 0 la 0 = \max_(i <- la) i.
proof: Proof. apply sorted_geq_nth0E. by have:= intpartnP la; rewrite is_part_sortedE => /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype