have : a = ((a / i) / 2) * (2 * i) + i + (a % i) := calc
  a = i * (a / i) + (a % i)                  := Eq.symm <| div_add_mod a i
  _ = i * (2 * ((a / i) / 2) + 1) + (a % i) := by simp [this]
  _ = ((a / i) / 2) * (2 * i) + i + (a % i) := by simp [mul_add, ←mul_assoc, mul_comm i 2, mul_comm (2 * i)]
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
⊢ ∃ k, ∃ r < i, a = k * (2 * i) + i + r
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