proposition: Lemma DP_NH1_prop3 b: starts_withFT b -> ~~(Dyck_NH1 b).
proof: Proof. rewrite starts_withFT_prop => /eqP ->; exact: (DP_NH1_prop2 (drop 2 b)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)