[STATEMENT]
lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset [m..<n] = mset_set {m..<n}
[PROOF STEP]
by (induction n) (simp_all add: atLeastLessThanSuc)