proposition: Lemma DP_splitc_rec l: DP_splitc l = if nilp l then [::] else if nilp (DP_splitb l).2 then [:: l] else rcons (DP_splitc (DP_splitb l).1) (DP_splitb l).2.
proof: Proof. have H: forall m n l, n <= m -> size l <= n -> DP_splitc_aux n l = DP_splitc_aux m l. clear l;elim => [n l | n Hr m l]; first by rewrite leqn0 => /eqP -> //. case: m; first by rewrite leqn0 => _ /nilP ->. move => m; rewrite ltnS => le1 le2 /=; case nn: (nilp l) => //. case nl1: (nilp _) => //. by rewrite (Hr _ _ le1 (leq_trans ( DP_splitb_size_rec nl1) le2)). rewrite /DP_splitc {1}/nilp. move: {-1}(size l) (erefl (size l));case => //= n eqa. case nn: (nilp (DP_splitb l).2); rewrite /nilp eqa //=. move:( DP_splitb_size_rec nn); rewrite eqa ltnS => sb. by rewrite (H _ _ _ sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)