proposition: Lemma DP_splita_correct l (a:= (DP_splita l).1 ) : (nilp a) || ((ends_withF a) && (Dyck_path ((DP_splita l).2))).
proof: Proof. rewrite/a; clear a; elim:l => // a l/=. set u := _.1; set v := _.2. case nu: (nilp u); [move => _ | by move/nilP: nu; case:u ]. have pl: DP_pos l by rewrite DP_splita_pos1. have ww:=(DP_posW pl). case:leqP => //=; rewrite /Dyck_path/DP_balanced pl /= eqn_leq ww !andbT. by case:a => //; rewrite add1n add0n ? ltnS // => /ltnW; rewrite ltnNge ww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)