rw [sq (a : ℤ), ← mul_assoc, ht, h1, mul_comm]
case intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℕ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * ↑c - 1)
h2 : c < a ∧ 0 < c
⊢ (n * ↑a ^ 2 - 1) ^ 2 = (n * ↑a * ↑c - 1) * (t * ↑b - 1)
no goals