induction y using hierarchy_polynomial_induction_oRing_sigma₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
⊢ ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hy : 0 < 0
⊢ ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'

case even
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝¹ : x✝ > 0
a✝ : 0 < x✝ → ∃ x < x✝, ∃ y' ≤ x✝, Exponential x y' ∧ x✝ < 2 * y'
hy : 0 < 2 * x✝
⊢ ∃ x < 2 * x✝, ∃ y' ≤ 2 * x✝, Exponential x y' ∧ 2 * x✝ < 2 * y'

case odd
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝ : 0 < x✝ → ∃ x < x✝, ∃ y' ≤ x✝, Exponential x y' ∧ x✝ < 2 * y'
hy : 0 < 2 * x✝ + 1
⊢ ∃ x < 2 * x✝ + 1, ∃ y' ≤ 2 * x✝ + 1, Exponential x y' ∧ 2 * x✝ + 1 < 2 * y'