proposition: Lemma cardinal_Dyck_path n: #|[set s: (n.*2).-tuple bool | Dyck_path s ]| = catalan n.
proof: Proof. case:n => //. rewrite /catalan /= bin0 divnn /=; apply:(eq_card1 (x:= [tuple ])) => s. by rewrite !inE; case: s => // u; case: u. move => n. rewrite catalan_pos //=. rewrite -(cardinal_tuple_nSSn n) - (cardinal_tuple_nm n.+1 n.*2.+2). rewrite - cardsDS; last by apply/subsetP => x; rewrite !inE => /andP[]. apply: eq_card => t; rewrite !inE. case h: (Dyck_path t); last by rewrite andbT; case: eqP => //. move /andP:h => [eqa _]; move/eqP:(DP_count t); rewrite size_tuple - (eqP eqa). by rewrite addnn - muln2 - {2} muln2 eqn_mul2r /= => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)