diff -r 070703d83cfe -r cec875dcc59e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon May 22 12:01:05 2023 +0200
+++ b/src/HOL/Nat.thy	Tue May 23 12:31:23 2023 +0100
@@ -2029,6 +2029,17 @@
 lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
   unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
 
+lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
+proof (intro iffI strict_monoI)
+  assume *: "\<forall>n. f n < f (Suc n)"
+  fix m n :: nat assume "m < n"
+  thus "f m < f n"
+    by (induction rule: less_Suc_induct) (use * in auto)
+qed (auto simp: strict_mono_def)
+
+lemma strict_mono_add: "strict_mono (\<lambda>n::'a::linordered_semidom. n + k)"
+  by (auto simp: strict_mono_def)
+
 lemma mono_nat_linear_lb:
   fixes f :: "nat \<Rightarrow> nat"
   assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"