exact sub_remove_left <| sub_remove_left <| by
  simp [add_assoc, show c + b = b + c from add_comm _ _, sub_add_self_of_le, ha]
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : b + c ≤ a
⊢ a - b - c = a - (b + c)
no goals