diff -r 9963bb965a0e -r 4bc4b5c0ccfc src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Jul 10 09:52:22 2018 +0100
+++ b/src/HOL/Power.thy	Tue Jul 10 23:18:08 2018 +0100
@@ -745,6 +745,12 @@
 lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
   using  abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less)
 
+lemma square_le_1:
+  assumes "- 1 \<le> x" "x \<le> 1"
+  shows "x\<^sup>2 \<le> 1"
+    using assms
+    by (metis add.inverse_inverse linear mult_le_one neg_equal_0_iff_equal neg_le_iff_le power2_eq_square power_minus_Bit0)
+
 end