src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Mon Mar 11 08:46:20 2024 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 11 15:07:02 2024 +0000
@@ -1926,6 +1926,9 @@
 lemma Nats_induct [case_names of_nat, induct set: Nats]: "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
   by (rule Nats_cases) auto
 
+lemma Nats_nonempty [simp]: "\<nat> \<noteq> {}"
+  unfolding Nats_def by auto
+
 end
 
 lemma Nats_diff [simp]: