apply le_eq_sub (Multiset.count x M) (Multiset.count x N) (Multiset.count x P) (Multiset.count x Q)
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x N = Multiset.count x Q + (Multiset.count x P - Multiset.count x M)
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M ≤ Multiset.count x P

case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
H0 : Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
l_u : Multiset.count x M ≤ Multiset.count x P
this : Multiset.count x Q ≤ Multiset.count x N
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q