--- a/src/HOL/Groups_List.thy Tue Nov 03 11:09:22 2020 +0100
+++ b/src/HOL/Groups_List.thy Tue Nov 03 12:57:18 2020 +0100
@@ -301,6 +301,10 @@
finally show ?thesis by(simp add:sum_list_map_eq_sum_count)
qed
+lemma sum_list_replicate: "sum_list (replicate n c) = of_nat n * c"
+by(induction n)(auto simp add: distrib_right)
+
+
lemma sum_list_nonneg:
"(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
by (induction xs) simp_all