fact: Fixpoint DP_resizeb (l: list (list bool)) := if l is a::l then let l' := DP_resizeb l in if (nilp l' || (starts_withFT (head nil l'))) then a::l' else (a ++ (head nil l')):: (behead l') else nil.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)