--- a/src/HOL/Library/Multiset_Order.thy Mon Jan 23 14:34:07 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Mon Jan 23 14:40:23 2023 +0100
@@ -138,8 +138,25 @@
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
+
subsubsection \<open>Properties of Preorders\<close>
+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
+ totalp_onD totalp_onI)
+
+lemma totalp_multp\<^sub>D\<^sub>M: "totalp R \<Longrightarrow> totalp (multp\<^sub>D\<^sub>M R)"
+ by (rule totalp_on_multp\<^sub>D\<^sub>M[of UNIV R UNIV, simplified])
+
+lemma totalp_on_multp\<^sub>H\<^sub>O:
+ "totalp_on A R \<Longrightarrow> (\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A) \<Longrightarrow> totalp_on B (multp\<^sub>H\<^sub>O R)"
+ by (smt (verit, ccfv_SIG) count_inI in_mono multp\<^sub>H\<^sub>O_def not_less_iff_gr_or_eq totalp_onD
+ totalp_onI)
+
+lemma totalp_multp\<^sub>H\<^sub>O: "totalp R \<Longrightarrow> totalp (multp\<^sub>H\<^sub>O R)"
+ by (rule totalp_on_multp\<^sub>H\<^sub>O[of UNIV R UNIV, simplified])
+
context preorder
begin