simpa using hm.lenbit_iff this pi.sq ltsqi
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
m✝ : M✝
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 j : M
pi : Pow2 i
pj : Pow2 j
hi : LenBit i m
hj : LenBit j m
hsqi : m < i ^ 2
hsqj : m < j ^ 2
ne : ¬i = j
hij : i < j
this : i ^ 2 ≤ m
ltsqi : 2 < i ^ 2
⊢ LenBit (i ^ 2) m ↔ LenBit i m
no goals