proposition: Lemma enum_partnP n p : (is_part_of_n n p) = (p \in enum_partn n).
proof: Proof. apply/idP/idP; last by move/(allP (enum_partn_allP n)). by rewrite -has_pred1 has_count; move/enum_partn_countE ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype