a : ℕ
a1 : 1 < a
n : ℕ
this : pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
have := pellZd_succ_succ a1 n
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    ↑(2 * a) * { re := ↑(xn a1 (n + 1)), im := ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
a : ℕ
a1 : 1 < a
n : ℕ
this : pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
unfold pellZd at this
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    { re := ↑(2 * a) * ↑(xn a1 (n + 1)), im := ↑(2 * a) * ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    ↑(2 * a) * { re := ↑(xn a1 (n + 1)), im := ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
erw [Zsqrtd.smul_val (2 * a : ℕ)] at this
a : ℕ
a1 : 1 < a
n : ℕ
h₁ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.re + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.re =
    ↑(2 * a) * ↑(xn a1 (n + 1))
h₂ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.im + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.im =
    ↑(2 * a) * ↑(yn a1 (n + 1))
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    { re := ↑(2 * a) * ↑(xn a1 (n + 1)), im := ↑(2 * a) * ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
injection this with h₁ h₂
no goals
a : ℕ
a1 : 1 < a
n : ℕ
h₁ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.re + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.re =
    ↑(2 * a) * ↑(xn a1 (n + 1))
h₂ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.im + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.im =
    ↑(2 * a) * ↑(yn a1 (n + 1))
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
constructor <;> apply Int.ofNat.inj <;> [simpa using h₁; simpa using h₂]