proposition: Theorem card_bal_Dyck_hsz n : #|bal_hsz n| = #|Dyck_hsz n| * n.+1.
proof: Proof. have -> : #|Dyck_hsz n| = #|preim_partition Dyck_of_bal (bal_hsz n)|. rewrite card_preim_partition; congr #|pred_of_set _|. apply/setP => /= w; apply/idP/imsetP => /= [|[u Hu ->{w}]]. - rewrite inE => HD. exists w; first by move: HD; rewrite !inE => /Dyck_wordP[_ ->]. by rewrite Dyck_of_Dyck_hsz. - by move: Hu; rewrite !inE /= => /eqP/Dyck_of_balP. apply: (card_uniform_partition _ (preim_partitionP Dyck_of_bal (bal_hsz n))). move=> /= B HB. have:= HB => /mem_preim_partition [/= w [Hw Heq]]. have {HB Hw} : w \in (bal_hsz n). have /and3P[/eqP Hcov _ _] := preim_partitionP Dyck_of_bal (bal_hsz n). by rewrite -Hcov; apply/bigcupP; exists B. rewrite inE => /eqP Hw. move: (Dyck_of_bal w) Heq (Dyck_of_balP Hw) => D Heq HD {w Hw}. by subst B; rewrite (card_preim_Dyck_of_bal HD). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree