diff -r 7f0edcc6c3d3 -r 91eae3a1be51 src/HOL/Library/Multiset_Order.thy
--- 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)