rw [← Int.modEq_zero_iff_dvd] at h ⊢
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
n : ℤ
a b : ℕ
h : ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
⊢ (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]