proposition: Lemma div_central_binomial n : n.+1 %| 'C(n.*2, n).
proof: Proof. by apply/dvdnP; exists #|Dyck_hsz n|; rewrite -card_bal_Dyck_hsz card_bal_hsz. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree