simp_all
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
b : M
a✝ : b > 0
IH✝ : ∀ {a : M}, a ⊆ b → a ≤ b
a : M
h : a ⊆ 2 * b
IH : a / 2 ≤ b
ha : 0 ∈ a
this : 0 ∈ 2 * b
⊢ False
no goals