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