proposition: Lemma enum_partns_allP sm sz : all (is_part_of_ns sm sz) (enum_partns sm sz).
proof: Proof. apply/allP; rewrite /enum_partns => /= p. case: sm => [/= | sm]; first by case: sz; rewrite //= mem_seq1 => /eqP ->. have /enum_partnsk_allP/allP Hall : sm.+1 >= 1 by []. by move=> /Hall /= /andP[_]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype