proposition: Lemma Dyck_sub_path' l1 l2: Dyck_path l2 -> Dyck_path (l1++l2) -> Dyck_path l1.
proof: Proof. move => /andP[sa sb] /andP[sc sd]. move: sa sc; rewrite /Dyck_path /DP_balanced /DP_Tcount /DP_Fcount. rewrite !count_cat => /eqP => sc; rewrite sc eqn_add2r => -> /=. elim: l1 sd {sb} => // a l Hr /= /andP[/Hr ]. by rewrite /DP_Fcount/DP_Tcount!count_cat sc !addnA leq_add2r => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)