proposition: Lemma enum_partnskE sm sz mx : mx >= 1 -> forall p, count_mem p (enum_partnsk sm sz mx) = is_part_of_nsk sm sz mx p.
proof: Proof. move=> Hx p; case (boolP ((is_part_of_nsk sm sz mx) p)) => H /=. - by rewrite enum_partnsk_countE. - apply/count_memPn; move: H; apply: contra. exact: (allP (enum_partnsk_allP _ _ Hx)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype