have : b * j + r < i * j :=
  pj.mul_add_lt_of_mul_lt_of_pos (by simp[pi, pj]) ((mul_lt_mul_right pj.pos).mpr hb)  hr (lt_of_lt_of_le hr $ le_mul_of_pos_left $ pi.pos)
case pos.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) + i + b)
⊢ LenBit (i * j) ((a * (2 * i) + i + b) * j + r)
case pos.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) + i + b)
this : b * j + r < i * j
⊢ LenBit (i * j) ((a * (2 * i) + i + b) * j + r)