rcases exponential_odd.mp H with ⟨y, rfl, H'⟩
case intro.inl.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
IH : ∀ y_1 < y, ∀ {x : M}, x < y_1 → (Exponential (x + 1) y_1 ↔ ∃ z ≤ y_1, y_1 = 2 * z ∧ Exponential x z)
x : M
hxy : 2 * x < y
H : Exponential (2 * x + 1) y
⊢ ∃ z ≤ y, y = 2 * z ∧ Exponential (2 * x) z
case intro.inl.mp.intro.intro
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 y
IH : ∀ y_1 < 2 * 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 < 2 * y ^ 2
H : Exponential (2 * x + 1) (2 * y ^ 2)
⊢ ∃ z ≤ 2 * y ^ 2, 2 * y ^ 2 = 2 * z ∧ Exponential (2 * x) z