added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff

--- a/NEWS	Mon May 08 11:16:45 2023 +0200
+++ b/NEWS	Mon May 08 11:24:46 2023 +0200
@@ -227,6 +227,8 @@
   - Used transp_on and reorder assumptions of lemmas bex_least_element and
     bex_greatest_element. Minor INCOMPATIBILITIES.
   - Added lemmas.
+      count_minus_inter_lt_count_minus_inter_iff
+      minus_inter_eq_minus_inter_iff
       mult_mono_strong
       multeqp_code_iff_reflclp_multp
       multp_code_iff_multp

--- a/src/HOL/Library/Multiset.thy	Mon May 08 11:16:45 2023 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon May 08 11:24:46 2023 +0200
@@ -375,6 +375,15 @@
   "a \<in># A + B \<longleftrightarrow> a \<in># A \<or> a \<in># B"
   by auto
 
+lemma count_minus_inter_lt_count_minus_inter_iff:
+  "count (M2 - M1) y < count (M1 - M2) y \<longleftrightarrow> y \<in># M1 - M2"
+  by (meson count_greater_zero_iff gr_implies_not_zero in_diff_count leI order.strict_trans2
+      order_less_asym)
+
+lemma minus_inter_eq_minus_inter_iff:
+  "(M1 - M2) = (M2 - M1) \<longleftrightarrow> set_mset (M1 - M2) = set_mset (M2 - M1)"
+  by (metis add.commute count_diff count_eq_zero_iff diff_add_zero in_diff_countE multiset_eq_iff)
+
 
 subsubsection \<open>Min and Max\<close>