have : M - N + P + N = M - N + N + P := by
  have : M - N + P + N = M - N + (P + N) := by
    apply add_assoc (M - N)
  rw [this]
  have : M - N + N + P = M - N + (N + P) := by apply add_assoc (M - N)
  rw [this]
  have : P + N = N + P := by apply add_comm P N
  simp_all only [ge_iff_le]
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P + N = M + P - N + N
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M - N + P + N = M + P - N + N