src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Mon Mar 22 00:07:55 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 22 10:49:51 2021 +0000
@@ -2027,6 +2027,10 @@
     by (cases "x \<in># A") simp_all
 qed
 
+lemma mset_set_upto_eq_mset_upto:
+  \<open>mset_set {..<n} = mset [0..<n]\<close>
+  by (induction n) (auto simp: ac_simps lessThan_Suc)
+
 context linorder
 begin