proposition: Lemma height_drop n u : height (drop n u) = height u - height (take n u).
proof: Proof. rewrite -{2}(cat_take_drop n u) height_cat. by rewrite addrC addrA [-_ + _]addrC subrr add0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree