Theorem: meq_union_meq_reverse (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N P : Multiset α
x✝ : M = N
⊢ M + P = N + P
Tactic:
simp_all only
State after:
no goals