src/HOL/Real.thy

--- a/src/HOL/Real.thy	Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Real.thy	Mon Jul 29 10:13:52 2024 +0100
@@ -1303,6 +1303,8 @@
   for x y :: real
   by auto
 
+lemma mult_ge1_I: "\<lbrakk>x\<ge>1; y\<ge>1\<rbrakk> \<Longrightarrow> x*y \<ge> (1::real)"
+  using mult_mono by fastforce
 
 subsection \<open>Lemmas about powers\<close>