proposition: Lemma height_take_leq (h : int) w : (forall n : nat, h <= height (take n w)) <-> (forall n : nat, (n <= size w)%N -> h <= height (take n w)).
proof: Proof. split => H n //; case (leqP n (size w)); first exact: H. move=> /ltnW/take_oversize ->. by rewrite -[w](take_oversize (leqnn _)); apply H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree