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