Change the one reference to dvd_sub to dvd_sub'

I would suggest removing it entirely but `Nat.dvd_sub` currently resides in the lean4 repo.

MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

@@ -130,7 +130,7 @@ theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p
 We can now prove the following formulation of our theorem.
 See if you can fill out the sketch.
 You can use ``Nat.factorial_pos``, ``Nat.dvd_factorial``,
-and ``Nat.dvd_sub``.
+and ``Nat.dvd_sub'``.
 BOTH: -/
 -- QUOTE:
 theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by