proposition: Lemma enum_partn_allP sm : all (is_part_of_n sm) (enum_partn sm).
proof: Proof. apply/allP; rewrite /enum_partn => /= p. case: sm => [/= | sm]; first by rewrite mem_seq1 => /eqP ->. rewrite cat0s => /flatten_mapP[i]. rewrite mem_iota ltnS => /andP[Hposi Hi]. have /enum_partnsk_allP/allP Hall : sm.+1 >= 1 by []. by move=> /Hall /= /and3P[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype