constructor
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 c : M
⊢ a = b - c * (b / c) ↔ ∃ x ≤ b, x = b / c ∧ a = b - c * x
case mp
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 c : M
⊢ a = b - c * (b / c) → ∃ x ≤ b, x = b / c ∧ a = b - c * x

case mpr
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 c : M
⊢ (∃ x ≤ b, x = b / c ∧ a = b - c * x) → a = b - c * (b / c)