exact ⟨(a / i) / 2, a % i, by simp [hi.pos], this⟩
case mp
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) + 1 = a / i
this : a = a / i / 2 * (2 * i) + i + a % i
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + i + r
no goals