proposition: Lemma rcons_bal_of_Dyck w k : (k <= size w)%N -> nth {{ (rcons w }}) (size w - k) = }} -> rcons (bal_of_Dyck k w) }} = rotr k (rcons w }}).
proof: Proof. move=> Hsz Hk; rewrite -cats1 -[RHS](cat_take_drop (size w)); congr (_ ++ _). apply (eq_from_nth (x0 := {{)) => [|i]. by rewrite size_drop /= size_rotr size_rcons subSn // subnn. rewrite /= ltnS leqn0 => /eqP->{i}. rewrite [LHS]/= nth_drop addn0 /rotr/rot nth_cat. rewrite !size_drop subKn; last by apply: (leq_trans Hsz); rewrite size_rcons. rewrite ltnNge Hsz /= nth_take; last by rewrite size_rcons subSn. by rewrite Hk. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree