# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1746388974 -3600
# Node ID f62666eea755bccd6bc17ff839f8671fab56e6b5
# Parent  328de89f20f9e54a17dc3f2f6c958ad91d76bb62
two more lemmas from the AFP

diff -r 328de89f20f9 -r f62666eea755 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun May 04 12:18:27 2025 +0100
+++ b/src/HOL/GCD.thy	Sun May 04 21:02:54 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 328de89f20f9 -r f62666eea755 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun May 04 12:18:27 2025 +0100
+++ b/src/HOL/Rings.thy	Sun May 04 21:02:54 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 +