intros M N h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
⊢ ∀ (M N : Multiset α), N ≤ M → M = M - N + N
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M - N + N