proposition: Lemma DP_splita_pos2 l: DP_pos (DP_splita l).2.
proof: Proof. elim:l => // a l Hr /=. case ha: (nilp (DP_splita l).1) => //. move: (DP_splita_recover l) Hr; move/nilP: ha => -> /= -> H. by case: leqP => //= ->; rewrite H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)