proposition: Lemma DP_NH1_prop4 a x: Dyck_path a -> starts_withFT x -> ~~(Dyck_NH1 (a ++ x)).
proof: Proof. rewrite starts_withFT_prop => ha /eqP ->. by move:(DP_NH1_prop1 (drop 2 x) ha); rewrite - catA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)