proposition: Lemma list_bool_decomp k lb : { ln : _ & { lc | lb = list_nat_bool ln ++ lc /\ Exists (fun x => k <= x) ln } } + { ln : _ & { r | lb = list_nat_bool ln ++ list_repeat Zero r /\ Forall (fun x => x < k) ln } }.
proof: Proof. induction lb as [ lb IH ] using (measure_rect (@length _)). destruct (list_bool_choose lb) as [ (x & lr & Hlb) | (x & Hlb) ]. * destruct (le_lt_dec k x) as [ Hk | Hk ]. + left; exists (x::nil), lr; split; simpl. - subst; solve list eq. - constructor 1; auto. + destruct (IH lr) as [ (ln & ld & H2 & H3) | (ln & r & H2 & H3) ]. - subst; rew length; lia. - left; exists (x::ln), ld; split. ** subst; solve list eq. ** constructor 2; auto. - right; exists (x::ln), r; split. ** subst; solve list eq. ** constructor; auto. * right; exists nil, x; split. - subst; solve list eq. - constructor. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)