a : ℕ
a1 : 1 < a
n : ℕ
this : 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * ↑a)
⊢ pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
have : (1 : ℤ√(d a1)) + ⟨a, 1⟩ * ⟨a, 1⟩ = ⟨a, 1⟩ * (2 * a) := by
  rw [Zsqrtd.coe_nat_val]
  change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩
  rw [dz_val]
  dsimp [az]
  rw [Zsqrtd.ext]
  dsimp
  constructor <;> ring_nf
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * { re := ↑a, im := 0 })
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * ↑a)
rw [Zsqrtd.coe_nat_val]
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1.re + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := 1.im + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          ↑(Pell.d a1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * { re := ↑a, im := 0 })
change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1.re + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := 1.im + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          (az a * az a - 1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1.re + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := 1.im + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          ↑(Pell.d a1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }
rw [dz_val]
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) } =
    { re := ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a),
      im := ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1.re + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := 1.im + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          (az a * az a - 1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }
dsimp [az]
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) }.re =
      { re := ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a),
          im := ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }.re ∧
    { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) }.im =
      { re := ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a),
          im := ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }.im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) } =
    { re := ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a),
      im := ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }
rw [Zsqrtd.ext]
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1) =
      ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a) ∧
    0 + (↑a * 1 + 1 * ↑a) = ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0)
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) }.re =
      { re := ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a),
          im := ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }.re ∧
    { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) }.im =
      { re := ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a),
          im := ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }.im
dsimp
no goals
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1) =
      ↑a * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (↑2 * 0 + 0 * ↑a) ∧
    0 + (↑a * 1 + 1 * ↑a) = ↑a * (↑2 * 0 + 0 * ↑a) + 1 * (↑2 * ↑a + (↑a * ↑a - 1) * 0 * 0)
constructor <;> ring_nf