proposition: Lemma enum_partnsk_allP sm sz mx : mx >= 1 -> all (is_part_of_nsk sm sz mx) (enum_partnsk sm sz mx).
proof: Proof. move=> Hmx; apply/allP => /=. elim: sz sm mx Hmx => [/= []| sz IHsz sm] //= mx Hmx p. by rewrite mem_seq1 => /eqP -> /=; rewrite Hmx. move/flatten_mapP => [i]. rewrite mem_iota ltnS => /andP[Hposi Himin] /mapP[recp]. move/(IHsz _ _ Hposi)/and4P => [Hp Hsum Hsz Hhead] -> /= {IHsz}. rewrite Hp (eqP Hsum) (eqP Hsz) Hhead {Hp Hsum Hsz Hhead} /=. move: Himin; rewrite leq_min => /andP[/subnKC -> ->]. by rewrite !eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype