rcases h with ⟨h, b, h0, k, h1⟩
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a ∧ ∃ b, a < b ∧ n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2
case intro.intro.intro.intro
n : ℤ
hn : 1 < n
a : ℕ
h : 0 < a
b : ℕ
h0 : a < b
k : ℤ
h1 : (n * ↑a ^ 2 - 1) ^ 2 = (n * ↑a * ↑b - 1) * k
⊢ ∃ c, 0 < c ∧ c < a ∧ n * ↑c * ↑a - 1 ∣ (n * ↑c ^ 2 - 1) ^ 2