diff -r c5059f9fbfba -r 250ab1334309 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Nov 26 11:14:10 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 27 10:01:40 2021 +0100
@@ -2819,6 +2819,18 @@
   assumes "r \<subseteq> r'" shows "mult r \<subseteq> mult r'"
   unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
 
+lemma mono_multp[mono]: "r \<le> r' \<Longrightarrow> multp r \<le> multp r'"
+  unfolding le_fun_def le_bool_def
+proof (intro allI impI)
+  fix M N :: "'a multiset"
+  assume "\<forall>x xa. r x xa \<longrightarrow> r' x xa"
+  hence "{(x, y). r x y} \<subseteq> {(x, y). r' x y}"
+    by blast
+  thus "multp r M N \<Longrightarrow> multp r' M N"
+    unfolding multp_def
+    by (fact mono_mult[THEN subsetD, rotated])
+qed
+
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   by (simp add: mult1_def)