proposition: Fact list_bool_next_neq_nil l : list_bool_next l <> nil.
proof: Proof. intros H. generalize (list_bool_next_spec l). rewrite H. apply list_bool_succ_neq_nil. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)