--- 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
--- 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>