# HG changeset patch
# User desharna
# Date 1683537405 -7200
# Node ID 0f92caebc19a3dd03590b95e94b615e33907fc9c
# Parent  ffdad62bc2354c0df68169b5fb502a766068c4ba
added lemma multpHO_implies_one_step_strong

diff -r ffdad62bc235 -r 0f92caebc19a NEWS
--- a/NEWS	Sun May 07 14:52:53 2023 +0100
+++ b/NEWS	Mon May 08 11:16:45 2023 +0200
@@ -247,6 +247,7 @@
       multpDM_mono_strong
       multpDM_plus_plusI[simp]
       multpHO_double_double[simp]
+      multpHO_implies_one_step_strong
       multpHO_mono_strong
       multpHO_plus_plus[simp]
       multpHO_repeat_mset_repeat_mset[simp]
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>