intro M N P h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
⊢ ∀ (M N P : Multiset α), N ≤ M → M - N + P = M + P - N
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
⊢ M - N + P = M + P - N