simpa using (show 1 < y^2 from lt_of_le_of_lt (by simp) hxy)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x y : M
H' : Exponential (x + 1) y
IH : ∀ y_1 < y ^ 2, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
hxy : 2 * x + 1 < y ^ 2
H : Exponential (2 * x + 1 + 1) (y ^ 2)
this : Exponential (2 * (x + 1)) (y ^ 2)
⊢ 1 < y
no goals