English
For a > 1 and m ≥ n, xz(a, m−n) = xz(a, m) xz(a, n) − d(a) yz(a, m) yz(a, n).
Русский
Для a > 1 и m ≥ n выполняется: xz(a, m−n) = xz(a, m) xz(a, n) − d(a) yz(a, m) yz(a, n).
LaTeX
$$$\\text{xz}^{(a)}(m-n) = \\text{xz}^{(a)}(m) \\cdot \\text{xz}^{(a)}(n) - d(a)\\, yz^{(a)}(m)\\, yz^{(a)}(n).$$$
Lean4
theorem xz_sub {m n} (h : n ≤ m) : xz a1 (m - n) = xz a1 m * xz a1 n - d a1 * yz a1 m * yz a1 n :=
by
rw [sub_eq_add_neg, ← mul_neg]
exact congr_arg Zsqrtd.re (pellZd_sub a1 h)