# HG changeset patch
# User desharna
# Date 1674834759 -3600
# Node ID bbe33afcfe1edee51ddd7f4e11992f2e5db392cf
# Parent  11d844d21f5cd2c16e9e6595456ffc523387642a# Parent  9678b533119e8da3458edd198943ce1fe76b4ae9
merged

diff -r 11d844d21f5c -r bbe33afcfe1e NEWS
--- a/NEWS	Fri Jan 27 13:57:52 2023 +0000
+++ b/NEWS	Fri Jan 27 16:52:39 2023 +0100
@@ -215,6 +215,7 @@
 * Theory "HOL-Library.Multiset_Order":
   - Added lemmas.
       irreflp_on_multpHO[simp]
+      multpHO_plus_plus[simp]
       totalp_multpDM
       totalp_multpHO
       totalp_on_multpDM
diff -r 11d844d21f5c -r bbe33afcfe1e src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Fri Jan 27 13:57:52 2023 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Fri Jan 27 16:52:39 2023 +0100
@@ -138,6 +138,9 @@
   using multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M[THEN multp\<^sub>D\<^sub>M_imp_multp] multp_imp_multp\<^sub>H\<^sub>O
   by blast
 
+lemma multp\<^sub>H\<^sub>O_plus_plus[simp]: "multp\<^sub>H\<^sub>O R (M + M1) (M + M2) \<longleftrightarrow> multp\<^sub>H\<^sub>O R M1 M2"
+  unfolding multp\<^sub>H\<^sub>O_def by simp
+
 
 subsubsection \<open>Properties of Preorders\<close>