--- a/src/HOL/Nat.thy Thu Nov 09 19:06:50 2023 +0100
+++ b/src/HOL/Nat.thy Thu Nov 09 15:11:51 2023 +0000
@@ -846,19 +846,21 @@
text \<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>.\<close>
-instance nat :: linordered_semidom
+instance nat :: discrete_linordered_semidom
proof
fix m n q :: nat
- show "0 < (1::nat)"
+ show \<open>0 < (1::nat)\<close>
by simp
- show "m \<le> n \<Longrightarrow> q + m \<le> q + n"
+ show \<open>m \<le> n \<Longrightarrow> q + m \<le> q + n\<close>
by simp
- show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n"
+ show \<open>m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n\<close>
by (simp add: mult_less_mono2)
- show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0"
+ show \<open>m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0\<close>
by simp
- show "n \<le> m \<Longrightarrow> (m - n) + n = m"
+ show \<open>n \<le> m \<Longrightarrow> (m - n) + n = m\<close>
by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
+ show \<open>m < n \<longleftrightarrow> m + 1 \<le> n\<close>
+ by (simp add: Suc_le_eq)
qed
instance nat :: dioid