proposition: Lemma DP_split_resize_flatten l: flatten l = flatten (DP_split_resize l).
proof: Proof. elim: l => // a l /= ->; case: (_ == _) => //. by case: (DP_split_resize l) => // 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)