proposition: Lemma Dyck_word_OwC w : w \is a Dyck_word -> {{ :: w ++ [:: }}] \is a Dyck_word.
proof: Proof. move/Dyck_wordP => [Hpos Hbal]; apply/Dyck_wordP; split => [n|]. - case: n => [|n /=]; first by rewrite take0. rewrite height_cons /=. case: (leqP n (size w)) => [/takel_cat -> | Hsz]. + by apply: (le_trans (Hpos n)); rewrite -subr_ge0 addrK. + rewrite take_oversize ?size_cat /= ?addn1 //. by rewrite !height_simpl /= addr0 addrC subrK -(take_size w). - by rewrite !height_simpl /= Hbal addr0 add0r subrr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree