proposition: Lemma DP_ph1_Dyck d : DP_ph1 d -> Dyck_path (flatten d).
proof: Proof. move/andP=> [_]; elim: d => // a l Hr /= /andP [ha hb]. exact: (Dyck_path_cat (DP_ph1_Dyck_aux ha) (Hr hb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)