src/HOL/Groups_List.thy

--- a/src/HOL/Groups_List.thy	Fri May 02 17:24:43 2025 +0200
+++ b/src/HOL/Groups_List.thy	Sun May 04 12:18:27 2025 +0100
@@ -665,4 +665,7 @@
   "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
   by (induction xs) simp_all
 
+lemma prod_list_nonneg: "(\<And> x. (x :: 'a :: ordered_semiring_1) \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> prod_list xs \<ge> 0"
+  by (induct xs) auto
+
 end