replace h := dvd_mul_of_dvd_left h ((n * b ^ 2) ^ 2)
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 * (n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2