proposition: Lemma Dyck_lp_Dyck n l: Dyck_path l -> size l = n.+1.*2 -> Dyck_path (Dyck_lp l).
proof: Proof. move => ha hb; rewrite /Dyck_lp. move:(DP_splitc_recover l)(DP_splitc_correct ha); case:(DP_splitc l). by move => hc; move:hb; rewrite -hc. move=> a s _ /= /andP[/andP [_ hd] he]; rewrite drop0;apply: (Dyck_path_cat hd). move: he; clear; elim:s => // a l Hr. move => /= /andP[ha hb] /=; rewrite - 2!cat_cons (Dyck_path_cat _ (Hr hb)) //. move/andP: ha =>[_ ha']; apply:(Dyck_path_cat DyckFT_Dyck ha'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)