lift c to ℕ using le_of_lt h2.2
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
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
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
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2