rcases (not_lenbit_iff_add_mul pi).mp h with ⟨a, b, hb, rfl⟩
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)
case neg.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i j r : M
pi : Pow2 i
pj : Pow2 j
hr : r < j
a b : M
hb : b < i
h : ¬LenBit i (a * (2 * i) + b)
⊢ ¬LenBit (i * j) ((a * (2 * i) + b) * j + r)