have : j^2 < i^2 := sq_lt_sq.mpr (lt_of_le_of_lt hj hz)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this : j < i ^ 2
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
⊢ Even (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j ∨
    Odd (Exponential.append (i ^ 2) X x) (Exponential.append (i ^ 2) Y y) j