--- a/src/HOL/Library/Multiset.thy Sat Nov 27 10:22:42 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Nov 27 10:28:48 2021 +0100
@@ -3140,6 +3140,11 @@
qed
qed
+lemma multp_code_eq_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multp_code r = multp r"
+ using multp_code_iff_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans multp_def, simplified]
+ by blast
+
lemma multeqp_code_iff_reflcl_mult:
assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
@@ -3154,6 +3159,12 @@
thus ?thesis using multp_code_iff_mult[OF assms] by simp
qed
+lemma multeqp_code_eq_reflclp_multp: "irreflp r \<Longrightarrow> transp r \<Longrightarrow> multeqp_code r = (multp r)\<^sup>=\<^sup>="
+ using multeqp_code_iff_reflcl_mult[of "{(x, y). r x y}" r for r,
+ folded irreflp_irrefl_eq transp_trans, simplified, folded multp_def]
+ by blast
+
+
subsubsection \<open>Partial-order properties\<close>
lemma mult1_lessE: