diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -1935,9 +1935,6 @@
 lemma ennreal_plus_if: "ennreal a + ennreal b = ennreal (if 0 \<le> a then (if 0 \<le> b then a + b else a) else b)"
   by (auto simp: ennreal_neg)
 
-lemma power_le_one_iff: "0 \<le> (a::real) \<Longrightarrow> a ^ n \<le> 1 \<longleftrightarrow> (n = 0 \<or> a \<le> 1)"
-  by (metis (mono_tags, opaque_lifting) le_less neq0_conv not_le one_le_power power_0 power_eq_imp_eq_base power_le_one zero_le_one)
-
 lemma ennreal_diff_le_mono_left: "a \<le> b \<Longrightarrow> a - c \<le> (b::ennreal)"
   using ennreal_mono_minus[of 0 c a, THEN order_trans, of b] by simp