English
For a > 1 and y ∈ ℕ, for all n, (2 a y − y^2 − 1) divides yz(a, n) (a − y) + y^n − xz(a, n).
Русский
Для a > 1 и y ∈ ℕ и любого n выполняется: (2 a y − y^2 − 1) делит yz(a, n)(a − y) + y^n − xz(a, n).
LaTeX
$$$\\bigl(2 a y - y^2 - 1\\bigr) \\mid \\bigl( yz^{(a)}(n)\\,(a - y) + y^n - xz^{(a)}(n) \\bigr)$$$
Lean4
theorem x_sub_y_dvd_pow (y : ℕ) : ∀ n, (2 * a * y - y * y - 1 : ℤ) ∣ yz a1 n * (a - y) + ↑(y ^ n) - xz a1 n
| 0 => by simp [xz, yz]
| 1 => by simp [xz, yz]
| n + 2 =>
by
have : (2 * a * y - y * y - 1 : ℤ) ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n) :=
⟨-↑(y ^ n), by
simp [_root_.pow_succ, mul_comm, mul_left_comm]
ring⟩
rw [xz_succ_succ, yz_succ_succ, x_sub_y_dvd_pow_lem ↑(y ^ (n + 2)) ↑(y ^ (n + 1)) ↑(y ^ n)]
exact _root_.dvd_sub (dvd_add this <| (x_sub_y_dvd_pow _ (n + 1)).mul_left _) (x_sub_y_dvd_pow _ n)
