fact: Fixpoint DP_splitb l := if l is a::l' then let u:= (DP_splitb l').1 in let v:= (DP_splitb l').2 in if(nilp u) then if (nilp v) then if a then ([::], [::a]) else ([::a], [::]) else if (DP_balanced v) then ([::a],v) else ([::],a::v) else (a::u,v) else ([::],[::]).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)