a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ 1
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
⊢ k ∣ 1
let p := pell_eq a1 n
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ 1
rw [← p]
no goals
a : ℕ
a1 : 1 < a
n k : ℕ
x✝ : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n = 1 := pell_eq a1 n
⊢ k ∣ xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n
exact Nat.dvd_sub (le_of_lt <| Nat.lt_of_sub_eq_succ p) (kx.mul_left _) (ky.mul_left _)