src/HOL/Power.thy

--- a/src/HOL/Power.thy	Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Power.thy	Mon Oct 04 12:32:50 2021 +0100
@@ -810,6 +810,10 @@
     by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
 qed
 
+lemma power2_le_iff_abs_le:
+  "y \<ge> 0 \<Longrightarrow> x\<^sup>2 \<le> y\<^sup>2 \<longleftrightarrow> \<bar>x\<bar> \<le> y"
+  by (metis abs_le_square_iff abs_of_nonneg)
+
 lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   using abs_le_square_iff [of x 1] by simp