no goals
α : Type u_1
β : Type ?u.1277
γ : Type ?u.1280
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t
rwa [cons_add, cons_add, zero_add] at s_eq