have : M = M - N + N := by
  apply mem_leq_diff
  exact h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P
⊢ M - N + N = M
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝¹ : M - N + P + N = M - N + N + P
this✝ : M + P - N + N = M + P
this : M = M - N + N
⊢ M - N + N = M