proposition: Lemma DP_splitb_Dyck12 l: Dyck_path l -> Dyck_path (DP_splitb l).1 && Dyck_path (DP_splitb l).2.
proof: Proof. move => h. move:(DP_splitb_pos2 l) (DP_splitb_recover l). case nl: (nilp (DP_splitb l).1); first by move/nilP:nl => -> _ //= ->. move => /= h1; rewrite h1 andbT => h2; rewrite - h2 in h. move: (DP_splitb l).1 (DP_splitb l).2 h1 h; clear; move=> u v /andP[/eqP hu _]. move/andP =>[sa sb]; apply /andP; split. rewrite /DP_balanced -(eqn_add2r (DP_Fcount v)) - {1} hu. by move: sa; rewrite /DP_balanced /DP_Tcount /DP_Fcount !count_cat. clear sa; elim: u sb => // a l H /= /andP [sa sb]. rewrite (H sa) /=. move: sb; rewrite /DP_Fcount /DP_Tcount !count_cat 2!addnA -/(DP_Tcount v). by rewrite hu leq_add2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)