proposition: Lemma DP_prop2 l k (l1 := take k l) (l2 := drop k l) : Dyck_path l -> (DP_Tcount l2 >= DP_Fcount l2) && (DP_Tcount l1 <= DP_Fcount l1).
proof: Proof. rewrite -(cat_take_drop k l) => /andP [ha hb]. suff h3:(DP_Tcount l2 >= DP_Fcount l2) by rewrite - (DP_count_sym ha) h3. move: hb; rewrite -/l2 -/l1;clear;elim l1; first exact:DP_posW. by move => a l3 Hr; rewrite cat_cons => /andP[ /Hr]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)