proposition: Lemma rrw_bal1 : height (rot rt (rcons w }})) = -1.
proof: Proof. rewrite /rot height_cat addrC -height_cat cat_take_drop. apply/eqP; rewrite height_simpl /= subr_eq. by move: HDyck => /Dyck_wordP[_ ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree