proposition: Lemma DP_splitb_pos2 l: nilp (DP_splitb l).1 || Dyck_path (DP_splitb l).2.
proof: Proof. elim: l => // a l /orP H /=. case hh:(nilp (DP_splitb l).1); last by case:H => //; rewrite hh. case nl: (nilp (DP_splitb l).2); first by case:a. rewrite /Dyck_path; case: ifP => // -> /=; clear; elim: l => // a l H /=. case: (nilp (DP_splitb l).1) => //. case:(nilp (DP_splitb l).2);first by case:a. case: ifP => //=; rewrite H /=. move: H; case: ((DP_splitb l).2) => // b s /andP [_ hb] hc. case:a; rewrite add0n add1n; first by apply: (leqW hb). by rewrite ltn_neqAle hb andbT eq_sym -/(DP_balanced _) hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)