[STATEMENT]
lemma less_eq_multiset_empty_right[simp]: "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}
[PROOF STEP]
by (metis less_eq_multiset_empty_left antisym)