proposition: Lemma bal_of_DyckK D rt : (rt <= size D)%N -> nth {{ (rcons D }}) (size D - rt) = }} -> tval D \is a Dyck_word -> Dyck_of_bal (bal_of_Dyck rt D) = D.
proof: Proof. move => Hsz Hnth Hw; apply val_inj; apply (@rconsK _ }} }}) => /=. set bD := take (size D) _. have -> : size bD = (size (rcons bD }})).-1 by rewrite size_rcons. rewrite (@rot_pfminhE (rcons bD }})); first last. rewrite /bD height_simpl /=. move: Hw => /Dyck_wordP[_] /(bal_of_DyckP Hsz Hnth) /= ->. by rewrite add0r. have {bD Hnth} -> : rcons bD }} = rotr rt (rcons D }}). rewrite {}/bD /rotr/rot take_cat size_drop subKn; first last. by rewrite size_rcons; apply: (leq_trans Hsz). rewrite ltnNge Hsz /= rcons_cat; congr (_ ++ _). rewrite size_rcons take_takel ?subSn //. by rewrite (take_nth {{) ?size_rcons ?ltnS ?leq_subr // Hnth. case: rt Hsz => [_ | rt Hsz]. rewrite /rotr subn0 rot_size -{1}(rot0 (rcons D }})) pfminh_rrw //. by rewrite subn0 -(size_rcons D }}) rot_size. rewrite pfminh_rrw // size_rcons; last by rewrite subSS leq_subr. rewrite subKn; last exact: (leq_trans Hsz). by rewrite rotrK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree