proposition: Lemma Dyck_path_exists1 n (l := (nseq n false) ++ (nseq n true)): (DP_Tcount l == n) && (Dyck_path l).
proof: Proof. have H1 m (v:bool) p: count p (nseq m v) = m * (p v). by elim:m => // m /= ->; rewrite mulSn. rewrite /Dyck_path /DP_balanced/DP_Tcount/DP_Fcount {1 2 3} /l. rewrite !count_cat !H1 /= muln0 muln1 addn0 eqxx /=. move:(leqnn n); rewrite /l; clear l; elim:{1 3}n. move => _ /=; elim:n => // n /= ->; rewrite /DP_Fcount /DP_Tcount !H1 //=. rewrite muln0 //. move => k H lkn /=; rewrite (H (ltnW lkn)) /= /DP_Tcount/DP_Fcount !count_cat. by rewrite !H1 /= !muln1 !muln0 // addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)