proposition: Lemma nth_pfminh : nth {{ w pfminh.-1 = }}.
proof: Proof. move: pfminhP pfminh_min pfminh_size. case: pfminh pfminh_pos => //= pfmh _ Hpfmh pfmh_min pfmh_sz. move/(_ _ (ltnSn pfmh)): pfmh_min => /=. move: Hpfmh; rewrite (take_nth {{ pfmh_sz) height_simpl /=. by case: nth => //= <- /ltW; rewrite lezD1 ltxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree