proposition: Lemma DP_splitc_recover l: flatten (DP_splitc l) = l.
proof: Proof. elim /size_ind:l => l Hr. rewrite (DP_splitc_rec l);case nn: (nilp l); first by move/nilP:nn => ->. case ha:(nilp (DP_splitb l).2); first by rewrite /= cats0. rewrite - cats1 flatten_cat (Hr _ (DP_splitb_size_rec ha)) /= cats0. by rewrite DP_splitb_recover. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)