[STATEMENT]
lemma mset_filter_mono:
  assumes "A \<subseteq># B" "\<And>x. x \<in># A \<Longrightarrow> P x \<Longrightarrow> Q x"
  shows   "filter_mset P A \<subseteq># filter_mset Q B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_mset P A \<subseteq># filter_mset Q B
[PROOF STEP]
by (rule mset_subset_eqI) (insert assms, auto simp: mset_subset_eq_count count_eq_zero_iff)