∀ {a : ℕ} (a1 : 1 < a) (n : ℕ) (x : ℤ)
  (motive :
    (y : ℤ) →
      0 < { re := 0, im := y + y } →
        { re := 0, im := y + y } < { re := 0, im := 1 + 1 } →
          1 ≤ { re := x, im := y } →
            Pell.IsPell { re := x, im := y } →
              { re := x, im := y } ≤ Pell.pellZd a1 (n + 1) →
                ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y } →
                  1 < { re := x, im := y } →
                    { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1 → Prop)
  (y : ℤ) (y0l : 0 < { re := 0, im := y + y }) (yl2 : { re := 0, im := y + y } < { re := 0, im := 1 + 1 })
  (h1 : 1 ≤ { re := x, im := y }) (hp : Pell.IsPell { re := x, im := y })
  (h : { re := x, im := y } ≤ Pell.pellZd a1 (n + 1)) (ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y })
  (h1l : 1 < { re := x, im := y })
  (bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1),
  (∀ (y0l : 0 < { re := 0, im := 0 + 0 }) (x_1 : { re := 0, im := 0 + 0 } < { re := 0, im := 1 + 1 })
      (h1 : 1 ≤ { re := x, im := 0 }) (hp : Pell.IsPell { re := x, im := 0 })
      (h : { re := x, im := 0 } ≤ Pell.pellZd a1 (n + 1)) (ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := 0 })
      (h1l : 1 < { re := x, im := 0 })
      (bm : { re := x, im := 0 } * { re := { re := x, im := 0 }.re, im := -{ re := x, im := 0 }.im } = 1),
      motive 0 y0l x_1 h1 hp h ha h1l bm) →
    (∀ (y : ℕ) (x_1 : 0 < { re := 0, im := ↑(y + 1) + ↑(y + 1) })
        (yl2 : { re := 0, im := ↑(y + 1) + ↑(y + 1) } < { re := 0, im := 1 + 1 }) (h1 : 1 ≤ { re := x, im := ↑(y + 1) })
        (hp : Pell.IsPell { re := x, im := ↑(y + 1) }) (h : { re := x, im := ↑(y + 1) } ≤ Pell.pellZd a1 (n + 1))
        (ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := ↑(y + 1) }) (h1l : 1 < { re := x, im := ↑(y + 1) })
        (bm :
          { re := x, im := ↑(y + 1) } *
              { re := { re := x, im := ↑(y + 1) }.re, im := -{ re := x, im := ↑(y + 1) }.im } =
            1),
        motive (Int.ofNat y.succ) x_1 yl2 h1 hp h ha h1l bm) →
      (∀ (a_1 : ℕ) (y0l : 0 < { re := 0, im := Int.negSucc a_1 + Int.negSucc a_1 })
          (x_1 : { re := 0, im := Int.negSucc a_1 + Int.negSucc a_1 } < { re := 0, im := 1 + 1 })
          (h1 : 1 ≤ { re := x, im := Int.negSucc a_1 }) (hp : Pell.IsPell { re := x, im := Int.negSucc a_1 })
          (h : { re := x, im := Int.negSucc a_1 } ≤ Pell.pellZd a1 (n + 1))
          (ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := Int.negSucc a_1 })
          (h1l : 1 < { re := x, im := Int.negSucc a_1 })
          (bm :
            { re := x, im := Int.negSucc a_1 } *
                { re := { re := x, im := Int.negSucc a_1 }.re, im := -{ re := x, im := Int.negSucc a_1 }.im } =
              1),
          motive (Int.negSucc a_1) y0l x_1 h1 hp h ha h1l bm) →
        motive y y0l yl2 h1 hp h ha h1l bm