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