obtain ⟨c, rfl⟩ : ∃ c : ℤ, k = t * c - 1 := by
  replace h1 : (t * a - 1) ^ 2 ≡ (t * b - 1) * k [ZMOD t] := by rw [h1]
  have X : ∀ m : ℤ, t * m - 1 ≡ -1 [ZMOD t] := fun m ↦ by
    symm; rw [Int.modEq_iff_dvd, sub_neg_eq_add, sub_add_cancel]; exact ⟨m, rfl⟩
  replace h1 := ((X a).pow 2).symm.trans (h1.trans ((X b).mul_right _))
  rw [Int.modEq_iff_dvd, sq, ← mul_sub, sub_neg_eq_add, neg_one_mul, dvd_neg] at h1
  cases' h1 with c h1
  exact ⟨c, eq_sub_of_add_eq h1⟩
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k t : ℤ
ht : n * ↑a = t
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
case intro.intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2