English
Let a > 1. If j ≤ n, then the Pell term satisfies xn(a1, 2n − j) + xn(a1, j) ≡ 0 (mod xn(a1, n)).
Русский
Пусть a > 1. При неотрицательных n, j с j ≤ n выполняется xn(a1, 2n − j) + xn(a1, j) ≡ 0 (mod xn(a1, n)).
LaTeX
$$$$ xn(a1, 2n - j) + xn(a1, j) \\equiv 0 \\pmod{ xn(a1, n) } $$$$
Lean4
theorem xn_modEq_x2n_sub_lem {n j} (h : j ≤ n) : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n] :=
by
have h1 : xz a1 n ∣ d a1 * yz a1 n * yz a1 (n - j) + xz a1 j :=
by
rw [yz_sub _ h, mul_sub_left_distrib, sub_add_eq_add_sub]
exact
dvd_sub
(by
delta xz; delta yz
rw [mul_comm (xn _ _ : ℤ)]
exact mod_cast (xn_modEq_x2n_add_lem _ n j))
((dvd_mul_right _ _).mul_left _)
rw [two_mul, add_tsub_assoc_of_le h, xn_add, add_assoc, ← zero_add 0]
exact (dvd_mul_right _ _).modEq_zero_nat.add (Int.natCast_dvd_natCast.1 <| by simpa [xz, yz] using h1).modEq_zero_nat
