[STATEMENT]
lemma singleton_times_left_hmset[simp]: "\<omega>^M * N = HMSet (image_mset ((+) M) (hmsetmset N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>^ M * N = HMSet (image_mset ((+) M) (hmsetmset N))
[PROOF STEP]
by (simp add: times_hmultiset_def Times_mset_single_left)