rcases H u hu ne2 ppu with (H | H)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y