proposition: Lemma DP_splitb_prop3 l: Dyck_path l -> ~~nilp l -> Dyck_irred (DP_splitb l).2.
proof: Proof. move => dl nl. have sa:= (DP_splitb_prop2a dl nl). move /andP:(DP_splitb_Dyck12 dl) => [_ /andP[ua' _]]. rewrite /Dyck_irred /Dyck_path - DP_count_catTF sa ua' eqxx /= DP_splita_pos1. move:(DP_splita_correct (DP_lower (DP_splitb l).2)); simpl. case ww: (nilp _) => //= /andP[ua ub]. move: sa; rewrite - (DP_splita_recover (DP_lower _)). set A := _.1; set B := _.2. rewrite /DP_raise rcons_cat -cat_cons (lastI false A) cat_rcons. have ->: (last false A = false) by move/eqP:ua; rewrite -/A;case: A. set s := false :: rcons B true => ee. move:(Dyck_path_augment ub); rewrite -/B -/s => ds. have ns: ~~ nilp s by rewrite /s /nilp. have: size (DP_splitb s).2 <= size s by rewrite-{2}(DP_splitb_recover s) size_cat leq_addl. move:(DP_splitb_race1 (belast false A) ds ns). rewrite ee (DP_splitb_race2 dl nl) => <-. rewrite - ee size_cat size_belast -{2}(add0n (size s)) leq_add2r leqn0. by rewrite -/(nilp A) ww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)