exact ⟨r, by
  by_contra A
  have hyv : b ≤ r := by simpa using A
  have : a < a := by calc
        a < b * (a / b + 1) := lt_mul_div_succ a hb
        _ ≤ b * (a / b) + r := by simpa [mul_add] using hyv
        _ = a               := e.symm
  simp at this, e⟩
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
⊢ ∃ r < b, a = b * (a / b) + r
no goals