proposition: Lemma Dyck_rp_prop l (u:= Dyck_rp_aux2 l) (u' := [seq Dyck_rp_aux s | s <- u]) : Dyck_path l -> [&& all DP_FT_DH1 u, flatten u == prependFT l, DP_splitc (flatten u') == u' & [seq Dyck_lp_aux s | s <- u'] == u ].
proof: Proof. move => dl. have ha:Dyck_path (prependFT l) by exact:(Dyck_path_cat DyckFT_Dyck dl). have hb: starts_withFT (prependFT l) by []. move:(DP_split_resizeb_correct ha hb). rewrite -/u; move/andP => [up flu]; rewrite up flu /=. have hu': (all Dyck_irred u'). apply/allP => x /mapP [y /(allP up) /andP [_ /andP [sa2 _]] ->]. by rewrite /Dyck_rp_aux /Dyck_irred DP_raiseK sa2 eqxx. rewrite /Dyck_lp (DP_splitc_unique hu' (erefl (flatten u'))) eqxx - map_comp. simpl; apply/eqP;apply: map_id_in => x /(allP up) /andP [ sa sb]. by apply:Dyck_rp_auxK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)