src/HOL/Library/Multiset.thy

 proof (rule mset_subset_eqI)
   fix x show "count (mset_set (set_mset A)) x \<le> count A x"
     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
 
 definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list"
 where