proposition: Theorem card_Dyck_hsz n : #|Dyck_hsz n| = Catalan n.
proof: Proof. by rewrite /Catalan -card_bal_hsz card_bal_Dyck_hsz mulnK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree