proposition: Lemma Dyck_path_augment l: Dyck_path l -> Dyck_path (DP_raise l).
proof: Proof. move/andP => [];rewrite -(DP_count_catTF l) /DP_raise => fa ub2. rewrite /Dyck_path /DP_pos -/DP_pos fa (eqP fa) leqnn /= andbT. elim:l ub2 {fa} => // a l H /= /andP [h1]. rewrite (H h1) /= - cats1 /DP_Fcount /DP_Tcount. rewrite !count_cat /= addn1 !addn0 addnS; apply: leqW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)