no goals
α : Type u_1
β : Type ?u.160229
γ : Type ?u.160232
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a✝ b a : α
s t : Multiset α
h : t ≤ s
⊢ a ::ₘ s - t = a ::ₘ (s - t)
rw [← singleton_add, ← singleton_add, add_tsub_assoc_of_le h]