proposition: Fact hookpartn_subproof d k : is_part_of_n d (hookpart d k).
proof: Proof. rewrite /hookpart /=; case: d => [|d]//. have /= /andP[/eqP -> ->] := colpartn_subproof (d.+1 - k.+1). rewrite andbT subSS minSS addSn minnE subnK ?leq_subr // eqxx /=. by case : (d - k). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype