proposition: Lemma intpartn_count_leq2E d (la : 'P_d) : (count (leq 2) la <= 1) = (nth 0 la 1 <= 1).
proof: Proof. apply: sorted_geq_count_leq2E. 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