ext b
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
⊢ X = a ::ₘ (M - {a0})
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
b : α
⊢ Multiset.count b X = Multiset.count b (a ::ₘ (M - {a0}))