proposition: Lemma starts_withFT_alt x: starts_withFT x = ((take 2 x) == DyckFT).
proof: Proof. by case:x => // a [ | b l]; case:a => //; case:b => //=;rewrite take0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)