by_contra ne
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
⊢ i = j
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
⊢ False