calc
  (a - b) * c = (a - b) * c + b * c - b * c := by simp
  _           = (a - b + b) * c - b * c     := by simp [add_mul]
  _           = a * c - b * c               := by simp [sub_add_self_of_le h]
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
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c = a * c - b * c
no goals