∀ {a k x y : ℕ},
  (∃ (a1 : 1 < a), Pell.xn a1 k = x ∧ Pell.yn a1 k = y) ↔
    1 < a ∧
      k ≤ y ∧
        (x = 1 ∧ y = 0 ∨
          ∃ u v s t b,
            x * x - (a * a - 1) * y * y = 1 ∧
              u * u - (a * a - 1) * v * v = 1 ∧
                s * s - (b * b - 1) * t * t = 1 ∧
                  1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])