have : M + P - N + N = M + P := by
  have : M + P - N + N = (M + P) ∪ N := by apply Eq.refl
  have : (M + P) ∪ N = M + P:= by
    apply Multiset.eq_union_left
    have : M ≤ M + P := by simp_all only [ge_iff_le, le_add_iff_nonneg_right, zero_le]
    apply le_trans h this
  simp_all only [ge_iff_le]
α : 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 + N + P = 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
this : M + P - N + N = M + P
⊢ M - N + N + P = M + P - N + N