diff --git a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
index 61a4cbeb..136799a3 100644
--- a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
+++ b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
@@ -306,8 +306,8 @@ we immediately have :math:`h(g(y))= y`, and we are done.
 
 Once again, we encourage you to step through the proof and fill in
 the missing parts.
-The tactic ``cases n with n`` splits on the cases ``g y ∈ sbAux f g 0``
-and ``g y ∈ sbAux f g n.succ``.
+The tactic ``rcases n with _ | n`` splits on the cases ``g y ∈ sbAux f g 0``
+and ``g y ∈ sbAux f g (n + 1)``.
 In both cases, calling the simplifier with ``simp [sbAux]``
 applies the corresponding defining equation of ``sbAux``.
 BOTH: -/
diff --git a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean
index 0657c90f..c159d6a9 100644
--- a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean
+++ b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean
@@ -344,12 +344,11 @@ we need to know that ``r`` is positive.
 But when ``r`` is zero, the theorem below is trivial, and easily
 proved by the simplifier.
 So the proof is carried out in cases.
-The line ``cases r with r`` replaces the goal with two versions:
+The line ``rcases r with _ | r`` replaces the goal with two versions:
 one in which ``r`` is replaced by ``0``,
-and the other in which ``r`` is replaces by ``r.succ``,
-the successor of ``r``.
+and the other in which ``r`` is replaces by ``r + 1``.
 In the second case, we can use the theorem ``r.succ_ne_zero``, which
-establishes ``r.succ ≠ 0``.
+establishes ``r + 1 ≠ 0`` (``succ`` stands for successor).
 
 Notice also that the line that begins ``have : npow_nz`` provides a
 short proof-term proof of ``n^k ≠ 0``.
@@ -359,9 +358,13 @@ and then think about how the tactics describe the proof term.
 See if you can fill in the missing parts of the proof below.
 At the very end, you can use ``Nat.dvd_sub'`` and ``Nat.dvd_mul_right``
 to finish it off.
+
+Note that this example does not assume that ``p`` is prime, but the
+conclusion is trivial when ``p`` is not prime since ``r.factorization p``
+is then zero by definition, and the proof works in all cases anyway.
 BOTH: -/
 -- QUOTE:
-example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} (prime_p : p.Prime) :
+example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} :
     k ∣ r.factorization p := by
   rcases r with _ | r
   · simp
@@ -372,8 +375,8 @@ example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} (
 SOLUTIONS: -/
     rw [factorization_pow']
 -- BOTH:
-  have eq2 : (r.succ * n ^ k).factorization p =
-      k * n.factorization p + r.succ.factorization p := by
+  have eq2 : ((r + 1) * n ^ k).factorization p =
+      k * n.factorization p + (r + 1).factorization p := by
 /- EXAMPLES:
     sorry
 SOLUTIONS: -/