rw [Int.modEq_iff_dvd, sub_neg_eq_add, sub_add_cancel]
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 [ZMOD t]
m : ℤ
⊢ -1 ≡ t * m - 1 [ZMOD t]
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 [ZMOD t]
m : ℤ
⊢ t ∣ t * m