# HG changeset patch
# User desharna
# Date 1683537964 -7200
# Node ID 3e5f6e31c4fd327fd92fc1d92aa3346063d67a4f
# Parent  0f7dc48d8b7fecd46704d9570621add8fa775fe1
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff

diff -r 0f7dc48d8b7f -r 3e5f6e31c4fd NEWS
--- a/NEWS	Mon May 08 11:24:46 2023 +0200
+++ b/NEWS	Mon May 08 11:26:04 2023 +0200
@@ -249,7 +249,9 @@
       multpDM_mono_strong
       multpDM_plus_plusI[simp]
       multpHO_double_double[simp]
+      multpHO_iff_set_mset_lessHO_set_mset
       multpHO_implies_one_step_strong
+      multpHO_minus_inter_minus_inter_iff
       multpHO_mono_strong
       multpHO_plus_plus[simp]
       multpHO_repeat_mset_repeat_mset[simp]
diff -r 0f7dc48d8b7f -r 3e5f6e31c4fd src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon May 08 11:24:46 2023 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Mon May 08 11:26:04 2023 +0200
@@ -192,6 +192,21 @@
     by (metis J_def K_def in_diff_count multp\<^sub>H\<^sub>O_def)
 qed
 
+lemma multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff:
+  fixes M1 M2 :: "_ multiset"
+  shows "multp\<^sub>H\<^sub>O R (M1 - M2) (M2 - M1) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2"
+  by (metis diff_intersect_left_idem multiset_inter_commute multp\<^sub>H\<^sub>O_plus_plus
+      subset_mset.add_diff_inverse subset_mset.inf.cobounded1)
+
+lemma multp\<^sub>H\<^sub>O_iff_set_mset_less\<^sub>H\<^sub>O_set_mset:
+  "multp\<^sub>H\<^sub>O R M1 M2 \<longleftrightarrow> (set_mset (M1 - M2) \<noteq> set_mset (M2 - M1) \<and>
+    (\<forall>y \<in># M1 - M2. (\<exists>x \<in># M2 - M1. R y x)))"
+  unfolding multp\<^sub>H\<^sub>O_minus_inter_minus_inter_iff[of R M1 M2, symmetric]
+  unfolding multp\<^sub>H\<^sub>O_def
+  unfolding count_minus_inter_lt_count_minus_inter_iff
+  unfolding minus_inter_eq_minus_inter_iff
+  by auto
+
 
 subsubsection \<open>Monotonicity\<close>