proposition: Lemma DP_split_resizeb_correct l (d := ( DP_resizeb (DP_split_resize (DP_splitc l)))): Dyck_path l -> starts_withFT l -> (all DP_FT_DH1 d) && (flatten d == l).
proof: Proof. rewrite starts_withFT_prop => ha hb. have ea: l = [::false ; true] ++ (drop 2 l) by rewrite {1} (eqP hb). have eb: Dyck_path [::false ; true] by []. rewrite ea in ha; move:(Dyck_sub_path eb ha) => dd. move: (DP_split_resize_correct3 dd). set x := DP_split_resize _; move => /andP[sa sb]. have dv: d = DP_resizeb (DyckFT :: x). by rewrite /d {1} ea (DP_splitc_cat eb dd). by rewrite dv (DP_resizeb_prop4 sa) - DP_resizeb_flatten /= eq_sym (eqP sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)