induction b using hierarchy_polynomial_induction_oRing_pi₁ generalizing a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a b : M
h : a ⊆ b
⊢ a ≤ b
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 {b} => ∀ {a : M}, a ⊆ b → a ≤ b

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
a : M
h : a ⊆ 0
⊢ a ≤ 0

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✝ : ∀ {a : M}, a ⊆ x✝ → a ≤ x✝
a : M
h : a ⊆ 2 * x✝
⊢ a ≤ 2 * x✝

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✝ : ∀ {a : M}, a ⊆ x✝ → a ≤ x✝
a : M
h : a ⊆ 2 * x✝ + 1
⊢ a ≤ 2 * x✝ + 1