[STATEMENT]
lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> M < {#}
[PROOF STEP]
using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M
[PROOF STATE]
proof (prove)
using this:
(?n \<subseteq># {#}) = (?n = {#})
(?M < ?N) = multp (<) ?M ?N
multp ?r ?M ?N = ((?M, ?N) \<in> mult {(x, y). ?r x y})
(?M < ?N) = (\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># ?N \<and> ?M = ?N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))

goal (1 subgoal):
 1. \<not> M < {#}
[PROOF STEP]
by blast