proposition: Lemma DP_splitb_size_correct l n (k := DP_splitb_size l): Dyck_path l -> size l = n.+1.*2 -> (size (DP_splitb l).2 == k.*2.+2) && (k <= n).
proof: Proof. move => sa sb. have nn: ~~ nilp l by rewrite /nilp sb. move/andP:(DP_splitb_prop3 sa nn) => [/eqP /(f_equal size) /= sc sd]. move: sc; rewrite size_rcons (Dyck_size_even sd) -/(DP_splitb_size l) -/k => ha. move/(f_equal size):(DP_splitb_recover l);rewrite sb size_cat ha eqxx /= => hb. by rewrite - ltnS - leq_double - hb leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)