proposition: Lemma Dyck_path_cat l1 l2: Dyck_path l1 -> Dyck_path l2 -> Dyck_path (l1 ++ l2).
proof: Proof. move =>/andP[/eqP ha hb] /andP[/eqP hc hd]. move: ha hc;rewrite/Dyck_path /DP_balanced /DP_Tcount /DP_Fcount !count_cat. by move => -> ->; rewrite eqxx (DP_pos_cat hb hd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)