[STATEMENT]
lemma size_multiset_eq_0_iff_empty [iff]:
  "size_multiset f M = 0 \<longleftrightarrow> M = {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (size_multiset f M = 0) = (M = {#})
[PROOF STEP]
by (auto simp add: size_multiset_eq count_eq_zero_iff)