proposition: Lemma minhP : forall i : nat, height (take i w) >= minh.
proof: Proof. rewrite /height minhE => i. wlog ilt : i / (i < (size w).+1)%N. move=> Hlog; case: (ltnP i (size w).+1) => [| szi]; first exact: Hlog. rewrite (take_oversize (ltnW szi)) -{9 10}(take_size w). exact: Hlog. case: (leqP (count_mem {{ (take i w)) (count_mem }} (take i w))) => [H|]. - rewrite -[i]/(nat_of_ord (Ordinal ilt)). rewrite lerNl opprB subzn // lez_nat. exact: leq_bigmax. - move=> /ltnW. rewrite -lez_nat -[in X in X -> _]subr_ge0 => /(le_trans _); apply. by rewrite -oppr_ge0 opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree