proposition: Lemma DP_split_resize_correct1 l: DP_ph1_aux (DP_split_resize l).
proof: Proof. elim:l => // al l Hr /=. case sz:(size al == 2);first by rewrite /= Hr /= sz. move: Hr; case: (DP_split_resize l)=> [ /= | b s /=]; first by rewrite orbT. case sb: (size b == 2); first by rewrite /= andbT sb /= orbT !andbT. by simpl => /andP[ ha hb]; rewrite ha /= hb orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)