proposition: Lemma Dyck_word_cat w1 w2 : w1 \is a Dyck_word -> w2 \is a Dyck_word -> w1 ++ w2 \is a Dyck_word.
proof: Proof. move=> /Dyck_wordP[Hpos1 Hbal1] /Dyck_wordP[Hpos2 Hbal2]. apply/Dyck_wordP; split => [n|]. - rewrite take_cat; case ltnP => _ //. by rewrite height_cat Hbal1 add0r. - by rewrite height_cat Hbal1 Hbal2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree