simp [mul_add, ←mul_assoc, mul_comm i 2, mul_comm (2 * i)]
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i a : M
hi : Pow2 i
h : ¬LenBit i a
this : 2 * (a / i / 2) = a / i
⊢ i * (2 * (a / i / 2)) + a % i = a / i / 2 * (2 * i) + a % i
no goals