English
Let a be a natural number with a > 1 and let x_n^{(a)} denote the Pell sequence associated to a. Then for all n, j ∈ ℕ, the Pell term at index 2n + j plus the Pell term at index j is congruent to 0 modulo the Pell term at index n: x_n^{(a)}(2n + j) + x_n^{(a)}(j) ≡ 0 (mod x_n^{(a)}(n)).
Русский
Пусть a ∈ ℕ и a > 1. Обозначим через x_n^{(a)} последовательность Пелля, связанную с a. Тогда для всех n, j ∈ ℕ выполняется конгруэнтность: x_n^{(a)}(2n + j) + x_n^{(a)}(j) ≡ 0 (mod x_n^{(a)}(n)).
LaTeX
$$$$ x_n^{(a)}(2n+j) + x_n^{(a)}(j) \\equiv 0 \\pmod{ x_n^{(a)}(n) } $$$$
Lean4
theorem xn_modEq_x2n_add (n j) : xn a1 (2 * n + j) + xn a1 j ≡ 0 [MOD xn a1 n] :=
by
rw [two_mul, add_assoc, xn_add, add_assoc, ← zero_add 0]
refine (dvd_mul_right (xn a1 n) (xn a1 (n + j))).modEq_zero_nat.add ?_
rw [yn_add, left_distrib, add_assoc, ← zero_add 0]
exact ((dvd_mul_right _ _).mul_left _).modEq_zero_nat.add (xn_modEq_x2n_add_lem _ _ _).modEq_zero_nat
