have : M - N + N + P = M - N + (N + P) := by apply add_assoc (M - N)
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + (P + N)
⊢ M - N + (P + N) = M - N + N + P
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + (P + N)
this : M - N + N + P = M - N + (N + P)
⊢ M - N + (P + N) = M - N + N + P