diff -r 6e2c6ccc5dc0 -r b4f892d0625d src/HOL/Library/Periodic_Fun.thy
--- a/src/HOL/Library/Periodic_Fun.thy	Tue Jan 24 23:05:32 2023 +0100
+++ b/src/HOL/Library/Periodic_Fun.thy	Wed Jan 25 13:37:44 2023 +0000
@@ -128,5 +128,25 @@
 
 interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}"
   by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1)
-  
+
+lemma cos_eq_neg_periodic_intro:
+  assumes "x - y = 2*(of_int k)*pi + pi \<or> x + y = 2*(of_int k)*pi + pi"
+  shows "cos x = - cos y" using assms
+proof
+  assume "x - y = 2 * (of_int k) * pi + pi" 
+  then show ?thesis
+    using cos.periodic_simps[of "y+pi"]
+    by (auto simp add:algebra_simps)
+next
+  assume "x + y = 2 * real_of_int k * pi + pi "
+  then show ?thesis
+    using cos.periodic_simps[of "-y+pi"]
+    by (clarsimp simp add: algebra_simps) (smt (verit))
+qed
+
+lemma cos_eq_periodic_intro:
+  assumes "x - y = 2*(of_int k)*pi \<or> x + y = 2*(of_int k)*pi"
+  shows "cos x = cos y"
+  by (smt (verit, ccfv_SIG) assms cos_eq_neg_periodic_intro cos_minus_pi cos_periodic_pi)
+
 end