proposition: Lemma enum_partnsE sm sz p : count_mem p (enum_partns sm sz) = is_part_of_ns sm sz p.
proof: Proof. case (boolP ((is_part_of_ns sm sz) p)) => H /=. - by rewrite enum_partns_countE. - apply/count_memPn; move: H; apply: contra. exact: (allP (enum_partns_allP _ _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype