diff -r 0b5efc6de385 -r b1d57dd345e1 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Filter.thy	Tue Dec 20 17:59:44 2022 +0000
@@ -1519,6 +1519,24 @@
     by eventually_elim (insert n, auto)
 qed
 
+lemma filterlim_minus_const_nat_at_top:
+  "filterlim (\<lambda>n. n - c) sequentially sequentially"
+  unfolding filterlim_at_top
+proof
+  fix a :: nat
+  show "eventually (\<lambda>n. n - c \<ge> a) at_top"
+    using eventually_ge_at_top[of "a + c"] by eventually_elim auto
+qed
+
+lemma filterlim_add_const_nat_at_top:
+  "filterlim (\<lambda>n. n + c) sequentially sequentially"
+  unfolding filterlim_at_top
+proof
+  fix a :: nat
+  show "eventually (\<lambda>n. n + c \<ge> a) at_top"
+    using eventually_ge_at_top[of a] by eventually_elim auto
+qed
+
 subsection \<open>Setup \<^typ>\<open>'a filter\<close> for lifting and transfer\<close>
 
 lemma filtermap_id [simp, id_simps]: "filtermap id = id"