diff --git a/GoldbachTm/Tm31/Content.lean b/GoldbachTm/Tm31/Content.lean
index 2e674ae..a9cb35c 100644
--- a/GoldbachTm/Tm31/Content.lean
+++ b/GoldbachTm/Tm31/Content.lean
@@ -20,6 +20,7 @@ refine (?_ ∘ g) ?_
   use (1+k)
   ring_nf at *
   simp [h]
+  omega
 . obtain ⟨x, y, _, hx, hy⟩ := hpp
   by_cases x ≤ y
   . use! x, y
diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
index 6bd6fbf..fccc23a 100644
--- a/GoldbachTm/Tm31/Prime.lean
+++ b/GoldbachTm/Tm31/Prime.lean
@@ -4,6 +4,7 @@ import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Transition
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.Nat.ModEq
+import Mathlib.Data.Nat.Prime.Basic
 
 namespace Tm31
 
diff --git a/GoldbachTm/Tm31/TuringMachine31.lean b/GoldbachTm/Tm31/TuringMachine31.lean
index 6ccb8c4..61c529a 100644
--- a/GoldbachTm/Tm31/TuringMachine31.lean
+++ b/GoldbachTm/Tm31/TuringMachine31.lean
@@ -1,6 +1,6 @@
 -- inspired by https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Computability/TuringMachine.lean
 import Mathlib.Computability.TuringMachine
-import Mathlib.Data.Real.Sqrt
+import Mathlib.Tactic.Ring.RingNF
 import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank