simp [hi.pos]
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
this : a = a / i / 2 * (2 * i) + a % i
⊢ a % i < i
no goals