rintro rfl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
i : M
pi : Pow2 i
him : i ≤ m
hsqi : (√i) ^ 2 = i
hi : LenBit (√i) m
ne1 : ¬i = 1
⊢ i ≠ 2
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
m : M
hm : SPPow2 m
pi : Pow2 2
him : 2 ≤ m
hsqi : (√2) ^ 2 = 2
hi : LenBit (√2) m
ne1 : ¬2 = 1
⊢ False