proposition: Lemma DP_splitc_unique l d: all Dyck_irred d -> flatten d = l -> DP_splitc l =d.
proof: Proof. elim /size_ind:l d => l Hr d hb hc. rewrite DP_splitc_rec; case nl: (nilp l). move: nl; rewrite -hc /nilp size_flatten; move/natnseq0P. move: hb; case d => // u v /= /andP [/andP[/eqP -> _] hv]. rewrite size_DP_raise //. move:(Dyck_flatten hb); rewrite hc => dl. rewrite (negbTE(DP_splitb_prop1 dl (negbT nl))). move /andP: (DP_splitb_Dyck12 dl) => [ha _]. have hd:= (DP_splitb_size_rec (negbTE (DP_splitb_prop1 dl (negbT nl)))). move: hb hc; case:d; first by move => _ ln; move: nl; rewrite -ln. move => a' d'; rewrite lastI; set a := last _ _; set d := belast _ _. rewrite -{1 2} cats1 all_cat flatten_cat /= cats0. move => /and3P[hu /andP[/eqP hv1 hv2] _] hw. have dpd:= (Dyck_flatten hu). move: (DP_splitb_recover l) => hw'. move:(DP_splitb_prop4 (Dyck_flatten hu) hv2); rewrite -hv1 hw. move/and3P => [eq1 /eqP /esym eq2 /eqP eq3]. by rewrite eq3 -(Hr (DP_splitb l).1 hd d hu eq2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)