feat(ch31): complete the Miller-Rabin error bound (Theorem 31.39, 4th ed.)

CLRSLean/Chapter_31.lean

@@ -30,19 +30,28 @@ primality test, and the Pollard's-rho factorization heuristic.
 
 ### 31.2 Greatest Common Divisor
 
-* {lit}`CLRS.Chapter31.euclid_recursion` (Lemma 31.2),
+* {lit}`CLRS.Chapter31.euclid_recursion` (Theorem 31.9, the GCD recursion
+  theorem),
   {lit}`CLRS.Chapter31.euclid` + {lit}`CLRS.Chapter31.euclid_eq_gcd`,
   {lit}`CLRS.Chapter31.gcd_is_linear_combination` (Lemma 31.3, Bezout),
   {lit}`CLRS.Chapter31.gcd_is_smallest_positive_linear_combination`
   (Theorem 31.2), the Corollary 31.3/31.4 facts, and
   {lit}`CLRS.Chapter31.extendedEuclid` + `extendedEuclid_spec`.
+* **Running time (Lamé / Fibonacci)**: {lit}`CLRS.Chapter31.euclidDivisions`
+  counts the recursive calls of `EUCLID`;
+  {lit}`CLRS.Chapter31.fib_le_of_euclidDivisions` (Lemma 31.10) gives
+  `a ≥ F_{k+2}`, `b ≥ F_{k+1}` for `k` calls;
+  {lit}`CLRS.Chapter31.euclidDivisions_lt` (Theorem 31.11, Lamé) bounds the
+  call count by `b < F_{k+1}`; and
+  {lit}`CLRS.Chapter31.euclidDivisions_le_two_log` (Corollary 31.12) is the
+  `O(log b)` bound.
 
 ### 31.3 Modular Arithmetic
 
 * {lit}`CLRS.Chapter31.mod_add` / `mod_mul` (Theorem 31.5),
   {lit}`CLRS.Chapter31.exists_mul_inverse_mod` (Theorem 31.6),
   {lit}`CLRS.Chapter31.mul_left_cancel_mod` (Theorem 31.9), and
-  {lit}`CLRS.Chapter31.modular_linear_solvable` (Theorem 31.11).
+  {lit}`CLRS.Chapter31.modular_linear_solvable` (Corollary 31.21).
 
 ### 31.4 Solving Modular Linear Equations
 
@@ -59,7 +68,7 @@ primality test, and the Pollard's-rho factorization heuristic.
 ### 31.6 Powers of an Element
 
 * {lit}`CLRS.Chapter31.modularExponentiation` + `modularExponentiation_spec`,
-  {lit}`CLRS.Chapter31.fermat_little_theorem` (Theorem 31.30), and
+  {lit}`CLRS.Chapter31.fermat_little_theorem` (Theorem 31.31), and
   {lit}`CLRS.Chapter31.euler_theorem`.
 
 ### 31.7 The RSA Public-Key Cryptosystem
@@ -72,22 +81,51 @@ primality test, and the Pollard's-rho factorization heuristic.
 * {lit}`CLRS.Chapter31.fermat_test` (Theorem 31.31),
   {lit}`CLRS.Chapter31.fermatPseudoprime`, and
   {lit}`CLRS.Chapter31.pseudoprime` + `pseudoprime_correct`.
+* **Carmichael numbers**: {lit}`CLRS.Chapter31.isCarmichael` — a composite `n`
+  passing the Fermat test for every coprime base
+  ({lit}`CLRS.Chapter31.carmichael_fermatPseudoprime`);
+  {lit}`CLRS.Chapter31.isCarmichael_561` exhibits the smallest one.
+* **Miller-Rabin**: {lit}`CLRS.Chapter31.strongTestParams` (the `2^s·d`
+  decomposition), {lit}`CLRS.Chapter31.strongPseudoprime` (STRONG-PSEUDOPRIME),
+  {lit}`CLRS.Chapter31.Witness`, and the executable
+  {lit}`CLRS.Chapter31.millerRabin` test.  Correctness:
+  {lit}`CLRS.Chapter31.strongPseudoprime_of_prime` (a prime passes every
+  base), {lit}`CLRS.Chapter31.not_witness_of_prime`, and
+  {lit}`CLRS.Chapter31.witness_not_prime` (a witness certifies
+  compositeness).
+* **Miller-Rabin error bound (Rabin–Monier)**: {lit}`CLRS.Chapter31.goodUnits`
+  (`S(n)`, the good subgroup), {lit}`CLRS.Chapter31.liar_mem_goodSet` (every
+  strong liar lies in `S(n)`), and the counting machinery
+  ({lit}`CLRS.Chapter31.card_pow_eq_one_crt`,
+  {lit}`CLRS.Chapter31.mTorsion_le_prod_half`).  The bound
+  {lit}`CLRS.Chapter31.goodUnits_card_le` proves `|S(n)| ≤ (n−1)/4` (three
+  cases: prime power, semiprime, and ≥3 prime factors), giving
+  {lit}`CLRS.Chapter31.strongLiars_card_le` — **at most `(n−1)/4` of the
+  bases are strong liars** (Theorem 31.39, sharpened to `(n−1)/4` by
+  Rabin–Monier).
 
 ### 31.9 Integer Factorization
 
+> ⚠️ **CLRS 4th edition removed this section** (integer factorization is no
+> longer in the main text of Chapter 31).  The POLLARD-RHO formalization is
+> retained for reference; a repo-wide migration will decide its fate.
+
 * {lit}`CLRS.Chapter31.rhoStep` and
   {lit}`CLRS.Chapter31.rho_collision_factor` (Pollard's rho).
+* **POLLARD-RHO**: {lit}`CLRS.Chapter31.RhoState` (tortoise-and-hare state),
+  {lit}`CLRS.Chapter31.pollardStep`, the loop {lit}`CLRS.Chapter31.pollardRhoLoop`,
+  and the full {lit}`CLRS.Chapter31.pollardRho` algorithm, with soundness
+  {lit}`CLRS.Chapter31.pollardRho_sound` (a returned factor is a nontrivial
+  divisor of `n`) and collision detection
+  {lit}`CLRS.Chapter31.pollardStep_collision_factor`.
 
-**Status: `selected-section-complete`** — Sections 31.1–31.9 fully proved.
+**Status: `selected-section-complete`** — Sections 31.1–31.9 fully proved,
+including the Miller-Rabin error bound.
 
 ## Deferred Work
 
-* 31.2 running-time (Lamé / Fibonacci) analysis of EUCLID.
-* 31.5 the general `k`-modulus CRT via `Nat.chineseRemainderOfList` /
-  `ZMod.chineseRemainder`.
-* 31.7 the RSA proof for messages sharing a factor with the modulus.
-* 31.8 Carmichael numbers and the Miller-Rabin test.
-* 31.9 the full Pollard's-rho algorithm and its birthday-paradox analysis.
+* 31.9 the birthday-paradox / expected-`O(√p)` running-time analysis of
+  POLLARD-RHO (a heuristic in CLRS, left informal).
 -/
 
 namespace CLRS

CLRSLean/Chapter_31/Section_31_2_Greatest_Common_Divisor.lean

@@ -15,6 +15,16 @@ Main results:
   `gcd(0, b) = b`, `gcd(a, 0) = a`.
 - {lit}`euclid` + {lit}`euclid_eq_gcd` + {lit}`euclid_terminates`: the EUCLID
   algorithm is a total function and always returns `Nat.gcd a b`.
+- **Running time (Lamé / Fibonacci)**: {lit}`euclidDivisions` counts the
+  recursive calls of `EUCLID`.  Lemma 31.10
+  ({lit}`fib_le_of_euclidDivisions`) gives the Fibonacci lower bounds
+  `a ≥ F_{k+2}` and `b ≥ F_{k+1}` for `k` calls; Theorem 31.11, **Lamé's
+  theorem** ({lit}`euclidDivisions_lt`), is the running-time bound
+  `b < F_{k+1} ⇒` fewer than `k` calls; and Corollary 31.12
+  ({lit}`euclidDivisions_le_two_log`) records the `O(log b)` bound.  The
+  helper lemmas {lit}`fib_two_step_ge_pow_two` and {lit}`pow_two_le_fib`
+  prove the exponential Fibonacci growth `2^(n/2) ≤ F_{n+2}` used by
+  Corollary 31.12.
 - Lemma 31.3 ({lit}`gcd_is_linear_combination`): **Bezout's identity** —
   `gcd a b` is an integer linear combination of `a` and `b`.
 - Theorem 31.2 ({lit}`gcd_is_smallest_positive_linear_combination`): `gcd a b`
@@ -35,10 +45,12 @@ Notation:
 - {lit}`Nat.gcdA a b` / {lit}`Nat.gcdB a b` : the Bezout coefficients.
 - `x·a + y·b` : integer linear combinations (coefficients in `ℤ`).
 
-Deferred: the running-time (Lamé / Fibonacci) analysis of EUCLID, and
-modular arithmetic, primality testing, and RSA (§31.3–31.9).
+This section is complete.  Modular arithmetic, primality testing, and RSA
+are covered in their own sections (§31.3–31.9).
 -/
 
+open Nat
+
 namespace CLRS
 
 namespace Chapter31
@@ -84,6 +96,181 @@ theorem euclid_eq_gcd (a b : ℕ) : euclid a b = Nat.gcd a b := by
 theorem euclid_terminates (a b : ℕ) : ∃ r : ℕ, euclid a b = r :=
   ⟨euclid a b, rfl⟩
 
+/--
+**EUCLID division count (CLRS §31.2).**  The number of recursive calls that
+`EUCLID(a, b)` makes under CLRS's recursion `EUCLID(a, b) = EUCLID(b, a mod b)`
+for `b > 0`, with `EUCLID(a, 0) = a`.  Total by well-founded recursion on the
+second argument (each call drops to `a mod b < b`).
+-/
+def euclidDivisions : ℕ → ℕ → ℕ
+  | _, 0 => 0
+  | a, b + 1 => 1 + euclidDivisions (b + 1) (a % (b + 1))
+termination_by _ b => b
+decreasing_by
+  exact Nat.mod_lt a (Nat.succ_pos b)
+
+/--
+**Lemma 31.10 (Lamé, core direction).**  If `EUCLID(a, b)` with `a > b ≥ 1`
+invokes `k` recursive calls, then the Fibonacci bounds `b ≥ F_{k+1}` and
+`a ≥ F_{k+2}` hold.
+-/
+theorem fib_le_of_euclidDivisions (a b : ℕ) (hb0 : 0 < b) (hba : b < a) :
+    fib (euclidDivisions a b + 1) ≤ b ∧ fib (euclidDivisions a b + 2) ≤ a := by
+  revert a hb0 hba
+  induction b using Nat.strong_induction_on with
+  | h b ih =>
+      intro a hb0 hba
+      cases b with
+      | zero => omega
+      | succ b' =>
+          let r := a % (b' + 1)
+          have hmain : euclidDivisions a (b' + 1) = 1 + euclidDivisions (b' + 1) r := by
+            simp [euclidDivisions, r]
+          by_cases hr0 : r = 0
+          · have hk1 : euclidDivisions a (b' + 1) = 1 := by
+              rw [hmain]
+              simp [euclidDivisions, r, hr0]
+            constructor
+            · rw [hk1]
+              simp [fib_two]
+            · rw [hk1]
+              simp [fib_add_two]
+              have hdvd : b' + 1 ∣ a := by
+                exact Nat.dvd_of_mod_eq_zero (by simpa [r] using hr0)
+              rcases hdvd with ⟨q, ha⟩
+              have hqb : b' + 1 < (b' + 1) * q := by
+                simpa [ha] using hba
+              have hq : 1 < q := by
+                exact (Nat.mul_lt_mul_left (by omega : 0 < b' + 1)).mp (by simpa using hqb)
+              have hle : 2 ≤ (b' + 1) * q := by
+                simpa using (Nat.mul_le_mul (by omega : 1 ≤ b' + 1) (Nat.succ_le_of_lt hq))
+              rw [ha]
+              exact hle
+          · have hrpos : 0 < r := Nat.pos_of_ne_zero hr0
+            have hrlt : r < b' + 1 := by
+              simpa [r] using (Nat.mod_lt a (Nat.succ_pos b'))
+            have ih' := ih r hrlt (b' + 1) hrpos hrlt
+            let k' := euclidDivisions (b' + 1) r
+            have hk' : euclidDivisions a (b' + 1) = 1 + k' := by
+              simpa [k'] using hmain
+            constructor
+            · rw [hk']
+              have harg : (1 + k') + 1 = k' + 2 := by omega
+              rw [harg]
+              simpa [k'] using ih'.2
+            · rw [hk']
+              have hfib3 : fib (k' + 3) = fib (k' + 1) + fib (k' + 2) := by
+                simpa [Nat.add_assoc] using (fib_add_two (n := k' + 1))
+              have hfib_sum : fib (k' + 1) + fib (k' + 2) ≤ r + (b' + 1) := by
+                exact Nat.add_le_add (by simpa [k'] using ih'.1) (by simpa [k'] using ih'.2)
+              have hra : r + (b' + 1) ≤ a := by
+                have hmod : a = a / (b' + 1) * (b' + 1) + r := by
+                  change a = a / (b' + 1) * (b' + 1) + a % (b' + 1)
+                  rw [mul_comm]
+                  exact (Nat.div_add_mod a (b' + 1)).symm
+                have hq1 : 1 ≤ a / (b' + 1) := by
+                  rw [Nat.le_div_iff_mul_le (Nat.succ_pos b')]
+                  simpa using (Nat.le_of_lt hba)
+                rw [hmod]
+                have hle : b' + 1 ≤ a / (b' + 1) * (b' + 1) := by
+                  simpa using (Nat.mul_le_mul_right (b' + 1) hq1)
+                omega
+              have harg : (1 + k') + 2 = k' + 3 := by omega
+              calc
+                fib ((1 + k') + 2) = fib (k' + 3) := by rw [harg]
+                _ = fib (k' + 1) + fib (k' + 2) := hfib3
+                _ ≤ r + (b' + 1) := hfib_sum
+                _ ≤ a := hra
+
+/--
+**Theorem 31.11 (Lamé's theorem).**  For `k ≥ 1`, if `a > b ≥ 1` and
+`b < F_{k+1}`, then `EUCLID(a, b)` makes fewer than `k` recursive calls —
+equivalently, `EUCLID` needs `O(log b)` calls for inputs `a > b`.
+-/
+theorem euclidDivisions_lt {a b k : ℕ} (_hk : 1 ≤ k) (hb0 : 0 < b) (hba : b < a)
+    (hbf : b < fib (k + 1)) : euclidDivisions a b < k := by
+  have hcore := fib_le_of_euclidDivisions a b hb0 hba
+  by_contra hnot
+  have hge : k ≤ euclidDivisions a b := Nat.le_of_not_gt hnot
+  have hmono : fib (k + 1) ≤ fib (euclidDivisions a b + 1) := by
+    exact fib_mono (by omega)
+  have : fib (k + 1) ≤ b := le_trans hmono hcore.1
+  exact (not_lt_of_ge this) hbf
+
+/--
+**Exponential Fibonacci growth.**  For every `t`, `fib(2t+2) ≥ 2^t` and
+`fib(2t+3) ≥ 2^t`; hence the Fibonacci sequence grows at least like
+`2^(n/2)`.  This is the exponential bound that turns Lamé's theorem into the
+`O(log b)` running-time bound.
+-/
+theorem fib_two_step_ge_pow_two (t : ℕ) :
+    (2 ^ t ≤ fib (2 * t + 2)) ∧ (2 ^ t ≤ fib (2 * t + 3)) := by
+  induction t with
+  | zero =>
+      constructor <;> norm_num [fib_two, fib_add_two, fib_one]
+  | succ t ih =>
+      have hA0 : 2 ^ t ≤ fib (2 * t + 2) := ih.1
+      have hB0 : 2 ^ t ≤ fib (2 * t + 3) := ih.2
+      have hA1 : 2 ^ (t + 1) ≤ fib (2 * (t + 1) + 2) := by
+        have hfib : fib (2 * (t + 1) + 2) = fib (2 * t + 2) + fib (2 * t + 3) := by
+          rw [show 2 * (t + 1) + 2 = 2 * t + 4 by ring]
+          have h := fib_add_two (n := 2 * t + 2)
+          rw [show (2 * t + 2) + 2 = 2 * t + 4 by omega,
+              show (2 * t + 2) + 1 = 2 * t + 3 by omega] at h
+          exact h
+        rw [hfib]
+        rw [show 2 ^ (t + 1) = 2 ^ t + 2 ^ t by rw [pow_succ]; ring]
+        exact Nat.add_le_add hA0 hB0
+      have hB1 : 2 ^ (t + 1) ≤ fib (2 * (t + 1) + 3) := by
+        have hfib : fib (2 * (t + 1) + 3) = fib (2 * t + 3) + fib (2 * t + 4) := by
+          rw [show 2 * (t + 1) + 3 = 2 * t + 5 by ring]
+          have h := fib_add_two (n := 2 * t + 3)
+          rw [show (2 * t + 3) + 2 = 2 * t + 5 by omega,
+              show (2 * t + 3) + 1 = 2 * t + 4 by omega] at h
+          exact h
+        rw [hfib]
+        have hA1' : 2 ^ (t + 1) ≤ fib (2 * t + 4) := by
+          simpa [show 2 * (t + 1) + 2 = 2 * t + 4 by ring] using hA1
+        exact le_trans (Nat.le_add_left _ _)
+          (by simpa [Nat.add_comm] using (Nat.add_le_add hB0 hA1'))
+      exact ⟨hA1, hB1⟩
+
+/-- The Fibonacci sequence grows exponentially: `2^(n/2) ≤ fib (n+2)` for all
+`n`. -/
+theorem pow_two_le_fib (n : ℕ) : 2 ^ (n / 2) ≤ fib (n + 2) := by
+  rcases Nat.even_or_odd n with ⟨t, rfl⟩ | ⟨t, rfl⟩
+  · have h2 : t + t = 2 * t := by omega
+    simpa [h2] using (fib_two_step_ge_pow_two t).1
+  · have hdiv : (2 * t + 1) / 2 = t := by
+      simpa [show 1 / 2 = 0 by norm_num] using (Nat.mul_add_div (by decide : 2 > 0) t 1)
+    rw [hdiv]
+    have harg : (2 * t + 1) + 2 = 2 * t + 3 := by omega
+    rw [harg]
+    exact (fib_two_step_ge_pow_two t).2
+
+/--
+**Corollary 31.12.**  For `a > b ≥ 1`, `EUCLID(a, b)` makes at most
+`2·log₂ b + 2` recursive calls — i.e. `O(log b)`.  Combining Lemma 31.10
+with `b ≥ F_{k+1} ≥ 2^{(k−1)/2}` bounds the division count logarithmically.
+-/
+theorem euclidDivisions_le_two_log (a b : ℕ) (hb0 : 0 < b) (hba : b < a) :
+    euclidDivisions a b ≤ 2 * Nat.log 2 b + 2 := by
+  have hkge1 : 1 ≤ euclidDivisions a b := by
+    rcases b with _ | b'
+    · omega
+    · simp [euclidDivisions]
+  have hcore := fib_le_of_euclidDivisions a b hb0 hba
+  have hpow_le_fib : 2 ^ ((euclidDivisions a b - 1) / 2) ≤ fib (euclidDivisions a b + 1) := by
+    have h := pow_two_le_fib (euclidDivisions a b - 1)
+    rwa [show (euclidDivisions a b - 1) + 2 = euclidDivisions a b + 1 by omega] at h
+  have hpow_le_b : 2 ^ ((euclidDivisions a b - 1) / 2) ≤ b := le_trans hpow_le_fib hcore.1
+  have hlog : (euclidDivisions a b - 1) / 2 ≤ Nat.log 2 b :=
+    Nat.le_log_of_pow_le (by decide : 1 < 2) hpow_le_b
+  have hk1 : euclidDivisions a b - 1 ≤ 2 * Nat.log 2 b + 1 := by
+    rw [Nat.div_le_iff_le_mul_add_pred (by decide : 0 < 2)] at hlog
+    exact hlog
+  omega
+
 /-- Lemma 31.3 (**Bezout's identity**): `gcd a b` is an integer linear
 combination of `a` and `b`. -/
 theorem gcd_is_linear_combination (a b : ℕ) :

CLRSLean/Chapter_31/Section_31_4_Solving_Modular_Linear_Equations.lean

@@ -16,6 +16,11 @@ Main results:
 - {lit}`linear_congruence_all_solutions`: if `x₀` and `x` both solve
   `a·x ≡ b (mod n)`, then `x ≡ x₀ (mod n/d)` — every solution differs from
   `x₀` by a multiple of `n/d`.
+- Theorem {lit}`linear_congruence_solutions` (Theorem 31.10): the solutions
+  are exactly the residue class `x₀ mod (n/d)`.
+- Theorem {lit}`linear_congruence_distinct` (Theorem 31.10): the `d` values
+  `k·(n/d)` for `0 ≤ k < d` are pairwise incongruent, so the congruence has
+  exactly `d` distinct solutions.
 
 Notation:
 
@@ -93,6 +98,63 @@ theorem linear_congruence_all_solutions {a b x x₀ n : ℕ} [NeZero n]
     exact Nat.coprime_div_gcd_div_gcd hd
   exact Nat.ModEq.cancel_left_of_coprime (by simpa [Nat.gcd_comm] using hcop'.gcd_eq_one) hax2
 
+/-- **The solutions of a linear congruence (CLRS Theorem 31.10).**  If `x₀`
+solves `a·x ≡ b (mod n)`, then a value `x` solves the congruence exactly when
+`x ≡ x₀ (mod n/d)` for `d = gcd(a, n)`: the solutions form one residue class
+modulo `n/d`. -/
+theorem linear_congruence_solutions {a b x₀ n : ℕ} [NeZero n] (h : a * x₀ ≡ b [MOD n]) :
+    ∀ x : ℕ, (a * x ≡ b [MOD n]) ↔ x ≡ x₀ [MOD (n / Nat.gcd a n)] := by
+  intro x
+  constructor
+  · intro hx
+    exact linear_congruence_all_solutions hx h
+  · intro hx
+    have h1 : a * x ≡ a * x₀ [MOD a * (n / Nat.gcd a n)] := by
+      rw [Nat.ModEq] at hx ⊢
+      rw [Nat.mul_mod_mul_left, Nat.mul_mod_mul_left]
+      rw [hx]
+    have h2 : a * x ≡ a * x₀ [MOD n] := by
+      rw [mul_nat_div_eq a n] at h1
+      exact Nat.ModEq.of_dvd (dvd_mul_left n (a / Nat.gcd a n)) h1
+    exact h2.trans h
+
+/-- **The `d = gcd(a, n)` solutions are distinct modulo `n` (CLRS Theorem
+31.10).**  The values `k·(n/d)` for `0 ≤ k < d` are pairwise incongruent
+modulo `n`, so together with {lit}`linear_congruence_shift` they give exactly
+`d` distinct solutions. -/
+theorem linear_congruence_distinct {a n : ℕ} [NeZero n] (k₁ k₂ : ℕ)
+    (hk₁ : k₁ < Nat.gcd a n) (hk₂ : k₂ < Nat.gcd a n) (hk : k₁ < k₂) :
+    ¬ k₁ * (n / Nat.gcd a n) ≡ k₂ * (n / Nat.gcd a n) [MOD n] := by
+  intro hc
+  have hd : n ∣ (k₂ - k₁) * (n / Nat.gcd a n) := by
+    have hle : k₁ * (n / Nat.gcd a n) ≤ k₂ * (n / Nat.gcd a n) := by
+      exact Nat.mul_le_mul_right _ (Nat.le_of_lt hk)
+    have hmod : (k₂ * (n / Nat.gcd a n) - k₁ * (n / Nat.gcd a n)) % n = 0 := by
+      have hsub := Nat.ModEq.sub (Nat.le_refl (k₁ * (n / Nat.gcd a n))) hle hc (Nat.ModEq.refl (k₁ * (n / Nat.gcd a n)))
+      have h0 : k₁ * (n / Nat.gcd a n) - k₁ * (n / Nat.gcd a n) = 0 := by omega
+      rw [h0] at hsub
+      simpa [Nat.ModEq, Nat.zero_mod] using hsub.symm
+    have hsub' : (k₂ - k₁) * (n / Nat.gcd a n) = k₂ * (n / Nat.gcd a n) - k₁ * (n / Nat.gcd a n) := by
+      rw [Nat.sub_mul]
+    rw [hsub']
+    exact Nat.dvd_of_mod_eq_zero hmod
+  have hn0 : 0 < n / Nat.gcd a n := by
+    exact Nat.div_pos (Nat.le_of_dvd (Nat.pos_of_neZero (n := n)) (Nat.gcd_dvd_right a n)) (Nat.gcd_pos_of_pos_right a (Nat.pos_of_neZero (n := n)))
+  have hpos : 0 < (k₂ - k₁) * (n / Nat.gcd a n) := by
+    have hk0 : 0 < k₂ - k₁ := by omega
+    exact Nat.mul_pos hk0 hn0
+  have hlt : (k₂ - k₁) * (n / Nat.gcd a n) < n := by
+    have hk2 : k₂ - k₁ < Nat.gcd a n := by omega
+    have hdn : (Nat.gcd a n) * (n / Nat.gcd a n) = n := Nat.mul_div_cancel' (Nat.gcd_dvd_right a n)
+    calc
+      (k₂ - k₁) * (n / Nat.gcd a n) < Nat.gcd a n * (n / Nat.gcd a n) := Nat.mul_lt_mul_of_pos_right hk2 hn0
+      _ = n := hdn
+  have hm0 : (k₂ - k₁) * (n / Nat.gcd a n) = 0 := by
+    have hmod : (k₂ - k₁) * (n / Nat.gcd a n) % n = 0 := Nat.mod_eq_zero_of_dvd hd
+    have hmod' : (k₂ - k₁) * (n / Nat.gcd a n) % n = (k₂ - k₁) * (n / Nat.gcd a n) := Nat.mod_eq_of_lt hlt
+    omega
+  omega
+
 end Chapter31
 
 end CLRS