src/HOL/Library/Multiset.thy

   if "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
   using that by (induction K) (simp_all add: add_mono)
 
 end
 
-context ordered_cancel_comm_monoid_diff
+context cancel_comm_monoid_add
 begin
 
 lemma sum_mset_diff:
   "sum_mset (M - N) = sum_mset M - sum_mset N" if "N \<subseteq># M" for M N :: "'a multiset"
   using that by (auto simp add: subset_mset.le_iff_add)