proposition: Lemma pfminh_min : forall i : nat, (i < pfminh)%N -> height (take i w) > minh.
proof: Proof. rewrite /pfminh. case: ex_minnP => pfmd /eqP Hpfmd pfmd_min i. rewrite ltnNge ltNge; apply contra => H. by apply pfmd_min; rewrite eq_le H minhP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree