proposition: Lemma DP_resizeb_prop2 l: all starts_withFT (DP_resizeb(DyckFT ::l)).
proof: Proof. move:(DP_resizeb_prop1 l) => /=;case: (DP_resizeb l) => // a s //=. by rewrite fun_if /= => ->; case:ifP => // ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)