fact: Definition hookpart d k := if d is d'.+1 then minn d'.+1 k.+1 :: nseq (d' - k) 1%N else [::].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype