src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Apr 27 11:21:04 2025 +0100
+++ b/src/HOL/Nat.thy	Fri May 02 16:25:38 2025 +0100
@@ -1793,12 +1793,12 @@
 
 class ring_char_0 = ring_1 + semiring_char_0
 
+lemma (in ordered_semiring_1) of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
+  by (induct n) simp_all
+
 context linordered_nonzero_semiring
 begin
 
-lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
-  by (induct n) simp_all
-
 lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
   by (simp add: not_less)