rw [mul_right_comm, sub_sq', add_comm, mul_right_comm _ _ (1 : ℤ), ← sub_sq']
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑b * ↑a - 1 ∣ (n * ↑b ^ 2 - 1) ^ 2
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2