# HG changeset patch
# User desharna
# Date 1677163037 -3600
# Node ID b23367be605163621aab5625f38253aeabd9486f
# Parent  347d7133c1716dfa306da4c6f5672866a0803f8f
added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO

diff -r 347d7133c171 -r b23367be6051 NEWS
--- a/NEWS	Thu Feb 23 12:35:37 2023 +0100
+++ b/NEWS	Thu Feb 23 15:37:17 2023 +0100
@@ -221,6 +221,8 @@
       multpDM_plus_plusI[simp]
       multpHO_mono_strong
       multpHO_plus_plus[simp]
+      strict_subset_implies_multpDM
+      strict_subset_implies_multpHO
       totalp_multpDM
       totalp_multpHO
       totalp_on_multpDM
diff -r 347d7133c171 -r b23367be6051 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Thu Feb 23 12:35:37 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Thu Feb 23 15:37:17 2023 +0100
@@ -168,6 +168,15 @@
 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
 
+lemma strict_subset_implies_multp\<^sub>D\<^sub>M: "A \<subset># B \<Longrightarrow> multp\<^sub>D\<^sub>M r A B"
+  unfolding multp\<^sub>D\<^sub>M_def
+  by (metis add.right_neutral add_diff_cancel_right' empty_iff mset_subset_eq_add_right
+      set_mset_empty subset_mset.lessE)
+
+lemma strict_subset_implies_multp\<^sub>H\<^sub>O: "A \<subset># B \<Longrightarrow> multp\<^sub>H\<^sub>O r A B"
+  unfolding multp\<^sub>H\<^sub>O_def
+  by (simp add: leD mset_subset_eq_count)
+
 
 subsubsection \<open>Monotonicity\<close>