proposition: Lemma Dyck_lpK n l: Dyck_NH2 l -> size l = n.+1.*2 -> Dyck_rp (Dyck_lp l) = l.
proof: Proof. move => /andP[ha hb] hc. have dlp:=(Dyck_lp_Dyck ha hc). have hd:= (DP_splitc_correct ha). move: hc;rewrite - {1 3} (DP_splitc_recover l). set sl := (DP_splitc l). case nl: (nilp sl); first by move/nilP:nl ->. move => _; clear n. have slv: sl = (head nil sl) :: behead sl by move: nl; clear; case:sl => //. rewrite /Dyck_lp/Dyck_rp /Dyck_rp_aux2 -/sl. set s1 := (flatten [seq Dyck_lp_aux s | s <- sl]). have s1v: s1 = (prependFT (drop 2 s1)) by rewrite /s1 -/sl slv /= drop0//. rewrite - s1v. have pa: Dyck_path s1. move:dlp;rewrite /Dyck_lp -/s1 {2} s1v => su. exact:(Dyck_path_cat DyckFT_Dyck su). have pb: starts_withFT s1 by rewrite s1v. move:(DP_split_resizeb_correct pa pb). set u := DP_resizeb _; move/andP=>[pc pd]. have ff: flatten u = flatten [seq Dyck_lp_aux s | s <- sl] by rewrite (eqP pd). have pc' : all DP_FT_DH1 [seq Dyck_lp_aux s | s <- sl]. apply/allP => x /mapP [y ysl ->]; rewrite/Dyck_lp_aux. move/(allP hd): (ysl) => /andP[_ qa2]. by move/(allP hb): ysl => qb; rewrite /DP_FT_DH1 /= drop0 /Dyck_NH1 qa2 qb. rewrite (DP_FT_DH1_unique pc pc' ff) - map_comp /comp map_id_in //. by move => x /(allP hd) /Dyck_lp_auxK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)