proposition: Lemma DP_resizeb_prop3 d: DP_ph1 d -> DP_resizeb_condition (DP_resizeb d).
proof: Proof. have eqA l: nilp l = nilp (DP_resizeb l). by clear; case:l => // a l /=; rewrite fun_if if_same. elim: d => // a d Hr /=; rewrite DP_ph1_simp => /and3P[ha hb hc]. move:(Hr ha); clear Hr; rewrite /DP_resizeb_condition. move: hb; case nd: (nilp d); first by move/nilP: nd => -> /= _; rewrite hc orbT. move: (nd); rewrite eqA => nrb; rewrite nrb /=. set b := (head [::] (DP_resizeb d)); set u := behead (DP_resizeb d). have eq1: (DP_resizeb d)= b :: u. by rewrite /b/u; move: nrb; case:(DP_resizeb d). move => hb /andP[hd he]; apply/orP; right. case /orP: he => he. by move /andP:(he) =>[-> _];rewrite /= eq1 /= hd hc he orbT. case/orP: he => he; first by rewrite (eqP he) /= eq1 hc /= hd (eqP he) orbT. move /andP:he => [he1 he2]. case ww:(starts_withFT b); first by move:(DP_NH1_prop3 ww); rewrite he2. have hw: ~~ nilp (a ++ b). by rewrite /nilp size_cat addn_eq0 -/(nilp b) (negbTE he1) andbF. case/orP:hb => hb; last first. have dv: d = (head [::] d) :: behead d by move: nd; clear; case:d. move: ha; rewrite dv /= DP_ph1_simp=> /and3P [_ _ aux1]. move: (DP_ph1_size2 aux1 hb) => hdv. by move:(DP_resizeb_prop2 (behead d)); rewrite -hdv - dv eq1 /= ww. move:(DP_ph1_size2 hc hb) => av. by rewrite hd /= /DP_ph1_aux2 hw /= /DP_FT_DH1 av /= drop0 he2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)