rw [← mul_pow, sub_one_mul, mul_mul_mul_comm, ← sq, ← mul_pow, ← mul_pow, ← mul_assoc] at h
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
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