proposition: Lemma DP_splita_recover l: (DP_splita l).1 ++ (DP_splita l).2 = l.
proof: Proof. elim: l => // a l /=. by case:(DP_splita l).1; [case: leqP | move => /= b l' {2} <-]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)