diff --git a/LeanTalkSP24/infinitely_many_primes.lean b/LeanTalkSP24/infinitely_many_primes.lean
index e6df1df..62fb34f 100644
--- a/LeanTalkSP24/infinitely_many_primes.lean
+++ b/LeanTalkSP24/infinitely_many_primes.lean
@@ -23,13 +23,15 @@ theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p
   have : m ≠ 0 := by
     intro mz
     rw [mz, zero_dvd_iff] at mdvdn
-    linarith
+    -- linarith
+    rw [mz, mdvdn] at mltn
+    contradiction
   have mgt2 : 2 ≤ m := two_le this mne1
   by_cases mp : m.Prime
   · use m, mp
   . rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
     use p, pp
-    apply pdvd.trans mdvdn
+    exact Nat.dvd_trans pdvd mdvdn
 
 theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by
   intro n