added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult

--- a/NEWS	Sun Feb 04 23:05:35 2024 +0100
+++ b/NEWS	Mon Feb 05 10:06:34 2024 +0100
@@ -40,6 +40,11 @@
 
 * Lemma even_succ_div_2 renamed to even_half_succ_eq.  Minor INCOMPATIBILITY.
 
+* Theory "HOL-Library.Multiset":
+  - Added lemmas.
+      trans_on_mult
+      transp_on_multp
+
 
 *** ML ***
 

--- a/src/HOL/Library/Multiset.thy	Sun Feb 04 23:05:35 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Feb 05 10:06:34 2024 +0100
@@ -3425,12 +3425,21 @@
   ultimately show thesis by (auto intro: that)
 qed
 
+lemma trans_on_mult:
+  assumes "trans_on A r" and "\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A"
+  shows "trans_on B (mult r)"
+  using assms by (metis mult_def subset_UNIV trans_on_subset trans_trancl)
+
 lemma trans_mult: "trans r \<Longrightarrow> trans (mult r)"
-  by (simp add: mult_def)
+  using trans_on_mult[of UNIV r UNIV, simplified] .
+
+lemma transp_on_multp:
+  assumes "transp_on A r" and "\<And>M. M \<in> B \<Longrightarrow> set_mset M \<subseteq> A"
+  shows "transp_on B (multp r)"
+  by (metis mult_def multp_def transD trans_trancl transp_onI)
 
 lemma transp_multp: "transp r \<Longrightarrow> transp (multp r)"
-  unfolding multp_def transp_trans_eq
-  by (fact trans_mult[of "{(x, y). r x y}" for r, folded transp_trans])
+  using transp_on_multp[of UNIV r UNIV, simplified] .
 
 lemma irrefl_mult:
   assumes "trans r" "irrefl r"