# HG changeset patch
# User desharna
# Date 1674483110 -3600
# Node ID e06463478a3fa322dd7674e7882267a44ad4868d
# Parent  4b37cc497d7efbe9ed80e62077930cf60a6ee8d4
added lemma irreflp_on_multpHO[simp]

diff -r 4b37cc497d7e -r e06463478a3f NEWS
--- a/NEWS	Mon Jan 23 14:40:23 2023 +0100
+++ b/NEWS	Mon Jan 23 15:11:50 2023 +0100
@@ -210,6 +210,7 @@
 
 * Theory "HOL-Library.Multiset_Order":
   - Added lemmas.
+      irreflp_on_multpHO[simp]
       totalp_multpDM
       totalp_multpHO
       totalp_on_multpDM
diff -r 4b37cc497d7e -r e06463478a3f src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Jan 23 14:40:23 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Jan 23 15:11:50 2023 +0100
@@ -141,6 +141,9 @@
 
 subsubsection \<open>Properties of Preorders\<close>
 
+lemma irreflp_on_multp\<^sub>H\<^sub>O[simp]: "irreflp_on B (multp\<^sub>H\<^sub>O R)"
+    by (simp add: irreflp_onI multp\<^sub>H\<^sub>O_def)
+
 lemma totalp_on_multp\<^sub>D\<^sub>M:
   "totalp_on A R \<Longrightarrow> (\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A) \<Longrightarrow> totalp_on B (multp\<^sub>D\<^sub>M R)"
   by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M not_less_iff_gr_or_eq