proposition: Lemma pfminhE n : (n <= size w)%N -> (forall i : nat, height (take i w) >= height (take n w)) -> (forall i : nat, (i < n)%N -> height (take i w) > height (take n w)) -> n = pfminh.
proof: Proof. move=> Hnsz Hleq Hltn. have Hnsz1 : (n < (size w).+1)%N by rewrite ltnS. have Hminh : height (take n w) = minh. by apply/eqP; rewrite eq_le minhP -pfminhP Hleq. rewrite Hminh in Hleq, Hltn. rewrite /pfminh; case: ex_minnP => pfmd /eqP Hpfmd pfmd_min. apply/anti_leq/andP; split. - move: Hpfmd => /eqP; rewrite eq_le => /andP[H _]. move: H; rewrite leNgt leqNgt; apply contra. exact: Hltn. - by apply pfmd_min; rewrite Hminh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree