proposition: Lemma DP_splitb_recover l: (DP_splitb l).1 ++ (DP_splitb l).2 = l.
proof: Proof. elim:l => // a l H /=. case ha: (nilp (DP_splitb l).1); last by rewrite /= H. move: H; move/nilP: ha => {1} -> /= ->. by case hb: (nilp l); [ move/nilP:hb => ->;case:a | case: ifP]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)