# HG changeset patch
# User desharna
# Date 1674818736 -3600
# Node ID 9678b533119e8da3458edd198943ce1fe76b4ae9
# Parent  780161d4b55c4199b767065af97e0e76791808bd
added lemma multpHO_plus_plus[simp]

diff -r 780161d4b55c -r 9678b533119e NEWS
--- a/NEWS	Thu Jan 26 13:59:51 2023 +0000
+++ b/NEWS	Fri Jan 27 12:25:36 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 780161d4b55c -r 9678b533119e src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Thu Jan 26 13:59:51 2023 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Fri Jan 27 12:25:36 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>