--- a/src/HOL/Library/Multiset_Order.thy Thu Oct 27 15:08:50 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Thu Oct 27 15:51:54 2016 +0200
@@ -280,6 +280,12 @@
unfolding less_multiset\<^sub>H\<^sub>O
by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
+lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \<longleftrightarrow> x < y"
+ unfolding less_multiset\<^sub>H\<^sub>O by simp
+
+lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
+ unfolding less_eq_multiset\<^sub>H\<^sub>O by force
+
instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)