proposition: Lemma DP_splitb_prop4 l1 l2 (s := l1 ++ DP_raise l2): Dyck_path l1 -> Dyck_path l2 -> [&& Dyck_path s, (DP_splitb s).1 == l1 & (DP_splitb s).2 == DP_raise l2 ].
proof: Proof. move => sa sb; set s':= DP_raise l2. have sc:=(Dyck_path_augment sb). rewrite (Dyck_path_cat sa sc). suff: (DP_splitb s).2 == s'. move => /eqP eq1. by move /eqP:(DP_splitb_recover s); rewrite eq1 {2}/s eqseq_catr eqxx => ->. suff: (DP_splitb s').2 == s'. rewrite /s; clear s sa => ww; elim:l1 => // a l H /=. case ha: (nilp _) => //;rewrite (eqP H) /=; move/andP:sc => [ -> //]. move: (DP_splitb_recover s');case (DP_splitb s').1; first by move /eqP. move => a u /eqP; rewrite /s' cat_cons eqseq_cons => /andP/proj2. have nn: ~~(nilp s') by rewrite /s' /nilp. move/andP :(DP_splitb_prop3 sc nn) => []; set v := DP_lower _ => /eqP -> hb. rewrite /DP_raise -rcons_cons - rcons_cat eqseq_rcons => /andP /proj1 hc. move/andP:(DP_prop2 (size u) sb) => /proj1; rewrite -(eqP hc) drop_size_cat //. move/andP:hb => [ /eqP];rewrite /DP_balanced /DP_Tcount /DP_Fcount /= => ->. by rewrite ltnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)