proposition: Lemma DP_resizeb_flatten l: flatten l = flatten (DP_resizeb l).
proof: Proof. elim: l => // a l /= ->; case:(DP_resizeb l); rewrite /= ? andbT ? andbF //. by move => b s /=; rewrite fun_if /= catA if_same. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)