diff -r ffdad62bc235 -r 0f92caebc19a src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sun May 07 14:52:53 2023 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Mon May 08 11:16:45 2023 +0200
@@ -177,6 +177,21 @@
   unfolding multp\<^sub>H\<^sub>O_def
   by (simp add: leD mset_subset_eq_count)
 
+lemma multp\<^sub>H\<^sub>O_implies_one_step_strong:
+  assumes "multp\<^sub>H\<^sub>O R A B"
+  defines "J \<equiv> B - A" and "K \<equiv> A - B"
+  shows "J \<noteq> {#}" and "\<forall>k \<in># K. \<exists>x \<in># J. R k x"
+proof -
+  show "J \<noteq> {#}"
+  using \<open>multp\<^sub>H\<^sub>O R A B\<close>
+  by (metis Diff_eq_empty_iff_mset J_def add.right_neutral multp\<^sub>D\<^sub>M_def multp\<^sub>H\<^sub>O_imp_multp\<^sub>D\<^sub>M
+      multp\<^sub>H\<^sub>O_plus_plus subset_mset.add_diff_inverse subset_mset.le_zero_eq)
+
+  show "\<forall>k\<in>#K. \<exists>x\<in>#J. R k x"
+    using \<open>multp\<^sub>H\<^sub>O R A B\<close>
+    by (metis J_def K_def in_diff_count multp\<^sub>H\<^sub>O_def)
+qed
+
 
 subsubsection \<open>Monotonicity\<close>