rw [← ht]
n : ℤ
hn : 1 + 1 ≤ n
a : ℕ
h : 0 + 1 ≤ ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 + 1 ≤ t
n : ℤ
hn : 1 + 1 ≤ n
a : ℕ
h : 0 + 1 ≤ ↑a
b : ℕ
h0 : a < b
t : ℤ
ht : n * ↑a = t
c : ℤ
h1 : (t * ↑a - 1) ^ 2 = (t * ↑b - 1) * (t * c - 1)
h2 : 0 ≤ n
⊢ 1 + 1 ≤ n * ↑a