proposition: Lemma DP_splitb_prop2a l (v:= (DP_splitb l).2) : Dyck_path l -> ~~nilp l -> DP_raise (DP_lower v) = v.
proof: Proof. move => dl nl. move /andP: (DP_splitb_Dyck12 dl) => [_ d2]. exact:(DP_lower_DyckK d2 (DP_splitb_prop1 dl nl)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)