diff --git a/GoldbachTm/Tm31/Prime.lean b/GoldbachTm/Tm31/Prime.lean
index 60daa02..f942d1e 100644
--- a/GoldbachTm/Tm31/Prime.lean
+++ b/GoldbachTm/Tm31/Prime.lean
@@ -99,18 +99,13 @@ induction rb with intros i la lb ra l r g hm
               obtain ⟨j, la', lb', g, h₁, h₂⟩ := g
               apply induction_step at g
               rw [← h₂] at g
-              have h : ra + 1 + 2 = ra + 3 := by omega
-              rw [h] at g
+              ring_nf at *
               specialize g h₁
               obtain ⟨k, la'', lb'', g, h₃, h₄⟩ := g
               use! (j+k), la'', lb''
+              ring_nf at *
               repeat any_goals constructor
-              any_goals tauto
-              . rw [← Nat.add_assoc i, g]
-                repeat any_goals first | omega | rfl | apply congr
-              . have h : ra + (rb + 1) +2 = ra + 1 + rb + 2:= by omega
-                rw [h]
-                assumption
+              all_goals tauto
 
 --    l 0 1 0  [lb 11]    0  0  [(rb+1) 1] 0 r
 --          c1            ^  c2