proposition: Lemma DP_ph1_Dyck_aux l: DP_ph1_aux2 l -> Dyck_path l.
proof: Proof. by case/orP; [move/eqP -> |move/andP=>[_ /andP[]] ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)