intro a b ha hb h0
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
⊢ ∀ (a b : ℕ), 0 < a → 0 < b → n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 → a = b
n : ℤ
hn : 1 < n
P : ℕ → Prop := fun k => 0 < k ∧ ∃ m, k < m ∧ n * ↑k * ↑m - 1 ∣ (n * ↑k ^ 2 - 1) ^ 2
h : ∀ (k : ℕ), ¬P k
a b : ℕ
ha : 0 < a
hb : 0 < b
h0 : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ a = b