proposition: Lemma hookpartnPE x0 x1 d (la : 'P_d) : nth x0 la 1 <= 1 -> la = hookpartn d (nth x1 la 0).-1.
proof: Proof. move=> H; apply val_inj => /=. case: la H => /= [[//=|l0 la] /andP[/eqP Heq Hpart]] /= H. by rewrite -Heq /hookpartn -lock. case: l0 Heq Hpart (part_head_non0 Hpart) => // l0 /=. rewrite addSn => [Hd] /andP[_ Hpart] _. rewrite hookpartnE -?Hd ?leq_addr // addKn. by rewrite {1}(part_nseq1P Hpart H). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype