# HG changeset patch
# User blanchet
# Date 1480404764 -3600
# Node ID 166a2563e0caa68c8e1bf4433c668a37afb6e02c
# Parent  a720c39113080d741265f4dd40afbeddeaa9aae7
added lemma about 'mult', as suggested by Bertram Felgenhauer

diff -r a720c3911308 -r 166a2563e0ca src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Nov 28 15:09:23 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Nov 29 08:32:44 2016 +0100
@@ -2825,6 +2825,9 @@
   thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
 qed
 
+lemmas mult_cancel_add_mset =
+  mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral]
+
 lemma mult_cancel_max:
   assumes "trans s" and "irrefl s"
   shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")