proposition: Lemma intpartn_leq p i : i \in pnval p -> i <= n.
proof: Proof. move=> /intpartn_leq_head /leq_trans; apply. by rewrite -(sumn_intpartn p); apply: leq_head_sumn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype