proposition: Lemma size_enum_partnsk sm sz mx : size (enum_partnsk sm sz mx) = (intpartnsk_nb sm sz mx).
proof: Proof. elim: sz sm mx => [ [] | sz IHsz] //= sm mx. rewrite size_flatten /shape -[1]addn0 iotaDl -!map_comp. rewrite (eq_map (g := fun i => intpartnsk_nb (sm - i.+1) sz i.+1)); first last. by move=> i /=; rewrite size_map IHsz. elim: (minn sm mx) => [// | n IHn]. by rewrite -{1}[n.+1]addn1 iotaD add0n map_cat sumn_cat IHn /= addn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype