proposition: Lemma DP_split_resize_correct3 l (d := (DP_split_resize (DP_splitc l))): Dyck_path l -> DP_ph1 d && (flatten d == l).
proof: Proof. move => ha; rewrite /d -DP_split_resize_flatten DP_splitc_recover. by rewrite (DP_split_resize_correct2 (DP_splitc_correct ha)) eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)