case even b _ IH =>
  have IH : a / 2 ≤ b := IH (by simpa using subset_div_two h)
  have : 2 * (a / 2) = a :=
    mul_div_self_of_dvd.mpr (zero_mem_iff.mp $ by intro ha; have : 0 ∈ 2 * b := h ha; simp_all)
  simpa [this] using mul_le_mul_left (a := 2) IH
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
⊢ a ≤ 2 * b
no goals