proposition: Lemma Dyck_word_OwCw w1 w2 : w1 \is a Dyck_word -> w2 \is a Dyck_word -> {{ :: w1 ++ }} :: w2 \is a Dyck_word.
proof: Proof. move=> Hw1 Hw2. rewrite -cat1s -[ }} :: _ ]cat1s !catA; apply Dyck_word_cat => //=. exact: Dyck_word_OwC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree