proposition: Lemma Dyck_path_exists2 n m (ln := (nseq n false) ++ (nseq n true)) (lm := (nseq m false) ++ (nseq m true)) (l := ln ++ DP_raise lm): [&& size l == (n+m).+1.*2, (Dyck_path l) & DP_splitb_size l == m].
proof: Proof. have sz: size (DP_raise lm) = (m.+1).*2. by rewrite size_DP_raise size_cat !size_nseq addnn. have ss: size l = ((n + m).+1).*2. by rewrite {1}/l/ln /= size_cat sz size_cat !size_nseq addnn -doubleD addnS. move: (Dyck_path_exists1 n) (Dyck_path_exists1 m). rewrite -/ln -/lm; move => /andP[ha hb]/andP[hc hd]. move:(DP_splitb_prop4 hb hd); rewrite -/l =>/and3P[qa qb /eqP qc]. rewrite ss eqxx qa; move/andP:(DP_splitb_size_correct qa ss) => [/eqP wa wb]. by rewrite - eqSS -eqn_double /= doubleS - wa qc sz eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)