proposition: Lemma size_enum_partn sm : size (enum_partn sm) = intpartn_nb sm.
proof: Proof. rewrite /intpartn_nb /enum_partn size_flatten /shape. elim: (sm.+1) => [// | n IHn]. rewrite -{1}[n.+1]addn1 iotaD add0n !map_cat sumn_cat IHn /= addn0. by rewrite size_enum_partns. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype