proposition: Fact nat_new_spec l : ~ In (nat_new l) l.
proof: Proof. assert (forall x, In x l -> x < nat_new l) as H. induction l as [ | x l IHl ]. intros _ []. intros y [ [] | Hy ]; apply le_n_S; [ apply Nat.le_max_l | ]. apply IHl, le_S_n in Hy. apply Nat.le_trans with (1 := Hy), Nat.le_max_r. intros C; apply H in C; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)