proposition: Lemma hookpartnE d k : k < d -> (hookpartn d k) = k.+1 :: nseq (d.-1 - k) 1%N :> seq nat.
proof: Proof. case: d => // d. by rewrite ltnS /hookpartn -lock /hookpart /= minSS => /minn_idPr ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype