proposition: Lemma bal_of_DyckP rt w : (rt <= size w)%N -> nth {{ (rcons w }}) (size w - rt) = }} -> height w = 0 -> height (bal_of_Dyck rt w) = 0.
proof: Proof. case: w => [w _] /= Hsz H H0. rewrite /rot take_cat size_drop size_rcons subKn; last exact: (leq_trans Hsz). rewrite ltnNge Hsz !height_simpl /= take_takel subSn // addrC. have : (size w - rt < size (rcons w }}))%N by rewrite size_rcons ltnS leq_subr. move=>/(take_nth {{)/(congr1 height); rewrite !height_simpl => /eqP. rewrite H /= -subr_eq opprK => /eqP <-. rewrite -addrA [(1 + _)%R]addrC addrA -height_cat cat_take_drop. by rewrite height_simpl! /= subrK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree