--- 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"