proposition: Lemma Dyck_word_flatten l : all (mem Dyck_word) l -> flatten l \is a Dyck_word.
proof: Proof. by elim: l => //= w l IHl /andP[Hd /IHl]; apply: Dyck_word_cat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree