proposition: Fact list_bool_choose lb : { k : _ & { tl | lb = list_repeat Zero k ++ One :: tl } } + { k | lb = list_repeat Zero k }.
proof: Proof. induction lb as [ | [] lb IHlb ]. * right; exists 0; auto. * left; exists 0, lb; auto. * destruct IHlb as [ (k & lc & H) | (k & H) ]. - left; exists (S k), lc; subst; auto. - right; exists (S k); subst; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)