no goals
α : Type u_1
β : Type ?u.308016
γ : Type ?u.308019
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ countp p (s - t) = countp p s - countp p t
simp [countp_eq_card_filter, h, filter_le_filter]