proposition: Lemma enum_partnsk_countE sm sz mx : mx >= 1 -> forall p, is_part_of_nsk sm sz mx p -> count_mem p (enum_partnsk sm sz mx) = 1.
proof: Proof. elim: sz sm mx => [| sz IHsz] /= sm mx Hmx. by move=> p /and4P[Hhead/nilP -> /= /eqP <-]. case=> [| p0 p] //=; first by rewrite andbF. move=> /and5P[Hp0]; rewrite eqSS=> /eqP Hsz /eqP Hsm Hhead Hpart. rewrite count_flatten -map_comp. rewrite (eq_map (g := fun i => i == p0 : nat)); first last. move=> i /=; rewrite count_map /=. case (i =P p0) => [Heq | /eqP/negbTE Hneq]. - subst p0; rewrite (eq_count (a2 := xpred1 p)); first last. by move=> s; rewrite /= -eqseqE /= eq_refl /=. rewrite {}IHsz //=. + have /part_head_non0 /= : is_part (i :: p) by rewrite /= Hhead Hpart. by rewrite lt0n. + by rewrite Hhead Hsz -Hsm addKn !eq_refl Hpart. - rewrite (eq_count (a2 := pred0)); first by rewrite count_pred0. by move=> s; rewrite /= -eqseqE /= Hneq. rewrite sumn_pred1_iota add1n ltnS leq_min Hp0 -Hsm leq_addr !andbT. have /part_head_non0 /= : is_part (p0 :: p) by rewrite /= Hhead Hpart. by rewrite lt0n => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype