# HG changeset patch
# User desharna
# Date 1683537886 -7200
# Node ID 0f7dc48d8b7fecd46704d9570621add8fa775fe1
# Parent  0f92caebc19a3dd03590b95e94b615e33907fc9c
added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff

diff -r 0f92caebc19a -r 0f7dc48d8b7f NEWS
--- 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
diff -r 0f92caebc19a -r 0f7dc48d8b7f src/HOL/Library/Multiset.thy
--- 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>