# HG changeset patch
# User desharna
# Date 1677151906 -3600
# Node ID 42accfbf4d850f906928972185cb2df08d2e637e
# Parent  c6e2c7887d4700f2ca1561832a4ab7956ea7e48f
added lemmas multpDM_mono_strong and multpHO_mono_strong

diff -r c6e2c7887d47 -r 42accfbf4d85 NEWS
--- a/NEWS	Wed Feb 22 22:01:26 2023 +0000
+++ b/NEWS	Thu Feb 23 12:31:46 2023 +0100
@@ -217,6 +217,8 @@
       asymp_multpHO
       asymp_not_liftable_to_multpHO
       irreflp_on_multpHO[simp]
+      multpDM_mono_strong
+      multpHO_mono_strong
       multpHO_plus_plus[simp]
       totalp_multpDM
       totalp_multpHO
diff -r c6e2c7887d47 -r 42accfbf4d85 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Wed Feb 22 22:01:26 2023 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Feb 23 12:31:46 2023 +0100
@@ -142,6 +142,19 @@
   unfolding multp\<^sub>H\<^sub>O_def by simp
 
 
+subsubsection \<open>Monotonicity\<close>
+
+lemma multp\<^sub>D\<^sub>M_mono_strong:
+  "multp\<^sub>D\<^sub>M R M1 M2 \<Longrightarrow> (\<And>x y. x \<in># M1 \<Longrightarrow> y \<in># M2 \<Longrightarrow> R x y \<Longrightarrow> S x y) \<Longrightarrow> multp\<^sub>D\<^sub>M S M1 M2"
+  unfolding multp\<^sub>D\<^sub>M_def
+  by (metis add_diff_cancel_left' in_diffD subset_mset.diff_add)
+
+lemma multp\<^sub>H\<^sub>O_mono_strong:
+  "multp\<^sub>H\<^sub>O R M1 M2 \<Longrightarrow> (\<And>x y. x \<in># M1 \<Longrightarrow> y \<in># M2 \<Longrightarrow> R x y \<Longrightarrow> S x y) \<Longrightarrow> multp\<^sub>H\<^sub>O S M1 M2"
+  unfolding multp\<^sub>H\<^sub>O_def
+  by (metis count_inI less_zeroE)
+
+
 subsubsection \<open>Properties of Preorders\<close>
 
 lemma irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"