proposition: Lemma DP_splitb_prop1 l: Dyck_path l -> ~~nilp l -> ~~(nilp ((DP_splitb l).2)).
proof: Proof. move => sa sb. move:(DP_splitb_lastT (false :: DP_lower l)). rewrite rcons_cons -/(DP_raise _) (DP_lower_DyckK sa sb). by case: (DP_splitb l).2 => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)