proposition: Lemma DP_resizeb_prop4 d: DP_ph1 d -> (all DP_FT_DH1 ((DP_resizeb (DyckFT :: d)))).
proof: Proof. move => h. move:(DP_resizeb_prop3 h);rewrite /DP_resizeb_condition /=. case nl: (nilp (DP_resizeb d)); first by move/nilP: nl ->. set b := (head [::] (DP_resizeb d)); set u := behead (DP_resizeb d). have eq1: (DP_resizeb d)= b :: u. by rewrite /b/u; move: nl; case:(DP_resizeb d). move=> /= /andP[ha hb]. case /orP: hb => hb. by move /andP:(hb) =>[-> _];rewrite eq1 /= ha hb. case/orP: hb => hb; first by rewrite (eqP hb) eq1 /= ha (eqP hb). move /andP:hb => [he1 he2]. case ww:(starts_withFT b); first by move:(DP_NH1_prop3 ww); rewrite he2. by rewrite /= ha /DP_FT_DH1 /= drop0 he2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)