by_cases h : LenBit i a <;> simp [h]
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
⊢ LenBit (i * j) (a * j + r) ↔ LenBit i a
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
h : LenBit i a
⊢ LenBit (i * j) (a * j + r)

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j a r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
h : ¬LenBit i a
⊢ ¬LenBit (i * j) (a * j + r)