proposition: Lemma DP_splitb_size_rec s: nilp (DP_splitb s).2 = false -> size (DP_splitb s).1 < size s.
proof: Proof. move => sa; rewrite - {2} (DP_splitb_recover s) size_cat -addn1 leq_add2l. by rewrite lt0n -/(nilp _) sa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)