have : M - N + P + N = M + P - N + N := by
  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]
  rw [this]
  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]
  rw [this]
  have : M - N + N = M := by
    have : M = M - N + N := by
      apply mem_leq_diff
      exact h
    rw [← this]
  simp_all only [ge_iff_le]
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P = M + P - N
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M + P - N + N
⊢ M - N + P = M + P - N