# HG changeset patch
# User blanchet
# Date 1487941189 -3600
# Node ID f6aea1a500ce7d6133583fa1809be408aa57a271
# Parent  18f3d341f8c0b6af6248353fa7fe1033faec3b6f
added multiset lemma

diff -r 18f3d341f8c0 -r f6aea1a500ce src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 24 13:24:55 2017 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 24 13:59:49 2017 +0100
@@ -2797,6 +2797,18 @@
   qed
 qed
 
+lemma subset_implies_mult:
+  assumes sub: "A \<subset># B"
+  shows "(A, B) \<in> mult r"
+proof -
+  have ApBmA: "A + (B - A) = B"
+    using sub by simp
+  have BmA: "B - A \<noteq> {#}"
+    using sub by (simp add: Diff_eq_empty_iff_mset subset_mset.less_le_not_le)
+  thus ?thesis
+    by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
+qed
+
 
 subsection \<open>The multiset extension is cancellative for multiset union\<close>