rw [mul_left_comm]
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ y * y < y * (2 * y)
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ y * y < 2 * (y * y)