proposition: Lemma DP_splitb_race1 s1 s2: Dyck_path s2 -> ~~ nilp s2 -> (DP_splitb (s1 ++ s2)).2 = (DP_splitb s2).2.
proof: Proof. move => ha hb; elim:s1 => //a l H /=. case: (nilp (DP_splitb (l ++ s2)).1) => //. rewrite H; move/andP:(DP_splitb_Dyck12 ha) =>[_ /andP [->]] /= _. by rewrite -(DP_splitb_prop2a ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)