have : √i ≤ ext i Y := le_trans (le_mul_of_pos_left $ by simp) this
case neg.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₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this✝ : ext i Y = 2 * ext (√i) Y ^ 2
this : 2 * √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2
case neg.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₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → y_1 ≤ ext y_1 Y ^ 2
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
IH : √i ≤ ext (√i) Y ^ 2
hodd : Seqₛ.Odd X Y (√i)
this✝¹ : ext i Y = 2 * ext (√i) Y ^ 2
this✝ : 2 * √i ≤ ext i Y
this : √i ≤ ext i Y
⊢ i ≤ ext i Y ^ 2