proposition: Lemma Dyck_rp_Dyck l: Dyck_path l -> Dyck_path (Dyck_rp l).
proof: Proof. have H s: (all Dyck_path s) -> Dyck_path (flatten s). elim:s => // a s H /= /andP[ha hb]; apply: (Dyck_path_cat ha (H hb)). have K x:DP_FT_DH1 x -> Dyck_path (Dyck_rp_aux x). move/andP => [sft /andP [hu hv]]; exact:(Dyck_path_augment hu). rewrite/Dyck_rp => dp; apply: H. have ha:Dyck_path (prependFT l) by exact:(Dyck_path_cat DyckFT_Dyck dp). have hb: starts_withFT (prependFT l) by []. move:(DP_split_resizeb_correct ha hb) => /andP[hc hd]. rewrite all_map; apply/allP => x /(allP hc) /=; apply:K. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)