# HG changeset patch
# User paulson
# Date 1746388984 -3600
# Node ID 43f4f9c5c6bdd2fcd6a3335ffebf77a87062d1e3
# Parent  98571d7e4a7dee41512f2a54f4fb7f896bda1b72# Parent  f62666eea755bccd6bc17ff839f8671fab56e6b5
merged

diff -r 98571d7e4a7d -r 43f4f9c5c6bd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun May 04 20:50:01 2025 +0200
+++ b/src/HOL/GCD.thy	Sun May 04 21:03:04 2025 +0100
@@ -2650,6 +2650,11 @@
   "\<bar>Gcd K\<bar> = Gcd K" for K :: "int set"
   by (simp only: Gcd_int_def)
 
+lemma uminus_Gcd_eq [simp]: 
+  fixes K::"int set"
+  shows "Gcd (uminus ` K) = Gcd K"
+  unfolding Gcd_int_def o_def by (simp add: image_image)
+
 lemma Gcd_int_greater_eq_0 [simp]:
   "Gcd K \<ge> 0"
   for K :: "int set"
diff -r 98571d7e4a7d -r 43f4f9c5c6bd src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun May 04 20:50:01 2025 +0200
+++ b/src/HOL/Rings.thy	Sun May 04 21:03:04 2025 +0100
@@ -2606,6 +2606,10 @@
 lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
   using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
 
+lemma less_1_mult': 
+  shows "1 < a \<Longrightarrow> 1 \<le> b \<Longrightarrow> 1 < a * b"
+  by (cases "b=1") (auto simp: le_less less_1_mult)
+
 end
 
 class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict +