proposition: Theorem list_bool_next_total l : l <> nil -> { n | l = iter list_bool_next (Zero::nil) n }.
proof: Proof. induction l as [ | l m Hlm IH ] using list_bool_succ_rect. intros []; auto. intros Hm. destruct (list_bool_choose_sym l) as [ (k & tl & H) | ([|k] & H) ]. * destruct IH as (n & Hn). { subst; destruct k; discriminate. } exists (n+1); rewrite iter_plus; simpl. rewrite <- Hn. generalize (list_bool_next_spec l). apply list_bool_succ_fun; auto. * exists 0; simpl. apply list_bool_succ_fun with (1 := Hlm). subst; simpl; constructor 2 with (k := 0). * destruct IH as (n & Hn). { subst; simpl; discriminate. } exists (n+1); rewrite iter_plus; simpl. rewrite <- Hn. generalize (list_bool_next_spec l). apply list_bool_succ_fun; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)