proposition: Lemma size_foldr_join_Dyck DS : (size (foldr join_Dyck nil_Dyck DS) = sumn (map (size \o dyckword) DS) + 2 * size DS)%N.
proof: Proof. elim: DS => //= D DS IHDS; rewrite size_cat /= IHDS. by rewrite -!addnS addnA mulnS [(2 + _)%N]addnC mul2n -addnn !addnA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree