proposition: Lemma hookpartnP d (la : 'P_d.+1) : reflect (exists k, k < d.+1 /\ la = hookpartn d.+1 k) (nth 0 la 1 <= 1).
proof: Proof. apply (iffP idP) => [H | ]. - exists (nth 0 la 0).-1; split; last exact: (hookpartnPE _ H). case: la H => /= [[//=|l0 la] /andP[/eqP Heq /part_head_non0]] /= Hl0 _. rewrite -ltnS -{}Heq /=; case: l0 Hl0 => // l0 _ /=. by rewrite addSn ltnS leq_addr. - move=> [k [lekd /(congr1 val) /= ->]]; rewrite hookpartnE // /=. by case: (d - k). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype