proposition: Fact iter_list_bool_next_nil l n : iter list_bool_next l n = nil -> n = 0 /\ l = nil.
proof: Proof. destruct n as [ | n ]. simpl; auto. replace (S n) with (n+1) by lia. rewrite iter_plus; simpl. intros H. apply list_bool_next_neq_nil in H. destruct H. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)