proposition: Lemma cardinal_tuple_nSSn n: #|[set s: (n.*2.+2).-tuple bool | (DP_Tcount s == n.+1) && ~~Dyck_path s ]| = 'C(n.*2.+2,n).
proof: Proof. move: (card_draws 'I_(n.*2.+2) n); rewrite card_ord => <-. rewrite cardinal_swap_but_last card_set_pred. rewrite -(card_imset _ (@list_to_set_inj (n.*2.+2)));apply: eq_card => x. rewrite !inE; apply/imsetP/idP => [ [y yp yv] | cx]. rewrite set_to_list_cardinal yv (list_to_setK (size_tuple y))//. have sm: size (char_seq x) == (n.*2.+2) by rewrite size_char_seq. set y:= Tuple sm. move:(list_to_setK (size_tuple y)) (set_to_listK x) => tt w. by exists y; rewrite ?w // inE - tt -set_to_list_cardinal w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)