# HG changeset patch
# User paulson
# Date 1633360278 -3600
# Node ID aca96bd12b12bcb658a8027c780de2b8198fab75
# Parent  e1b5bf983de36a6d300df3cc385f8646bd05d450# Parent  c278b186459227c79596a4be8028e283cd90badd
merged

diff -r e1b5bf983de3 -r aca96bd12b12 src/HOL/Analysis/Ball_Volume.thy
--- a/src/HOL/Analysis/Ball_Volume.thy	Mon Oct 04 15:01:50 2021 +0200
+++ b/src/HOL/Analysis/Ball_Volume.thy	Mon Oct 04 16:11:18 2021 +0100
@@ -1,4 +1,4 @@
-(*  
+(*
    File:     HOL/Analysis/Ball_Volume.thy
    Author:   Manuel Eberl, TU München
 *)
@@ -25,11 +25,11 @@
 
 text \<open>
   We first need the value of the following integral, which is at the core of
-  computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an 
+  computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an
   \<open>n\<close>-dimensional one.
 \<close>
 lemma emeasure_cball_aux_integral:
-  "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) = 
+  "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
       ennreal (Beta (1 / 2) (real n / 2 + 1))"
 proof -
   have "((\<lambda>t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral
@@ -37,7 +37,7 @@
     using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp
   from nn_integral_has_integral_lebesgue[OF _ this] have
      "ennreal (Beta (1 / 2) (real n / 2 + 1)) =
-        nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) * 
+        nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) *
                                 indicator {0^2..1^2} t))"
     by (simp add: mult_ac ennreal_mult' ennreal_indicator)
   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
@@ -45,7 +45,7 @@
     by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
        (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
   also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
-    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) 
+    by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"])
        (auto simp: indicator_def powr_minus powr_half_sqrt field_split_simps ennreal_mult')
   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
                     (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
@@ -54,7 +54,7 @@
     by (subst nn_integral_real_affine[of _ "-1" 0])
        (auto simp: indicator_def intro!: nn_integral_cong)
   hence "?I + ?I = \<dots> + ?I" by simp
-  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * 
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) *
                     (indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
     by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
@@ -69,13 +69,10 @@
 lemma real_sqrt_le_iff': "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> y ^ 2"
   using real_le_lsqrt sqrt_le_D by blast
 
-lemma power2_le_iff_abs_le: "y \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
-  by (subst real_sqrt_le_iff' [symmetric]) auto
-
 text \<open>
-  Isabelle's type system makes it very difficult to do an induction over the dimension 
-  of a Euclidean space type, because the type would change in the inductive step. To avoid 
-  this problem, we instead formulate the problem in a more concrete way by unfolding the 
+  Isabelle's type system makes it very difficult to do an induction over the dimension
+  of a Euclidean space type, because the type would change in the inductive step. To avoid
+  this problem, we instead formulate the problem in a more concrete way by unfolding the
   definition of the Euclidean norm.
 \<close>
 lemma emeasure_cball_aux:
@@ -92,17 +89,17 @@
   case (insert i A r)
   interpret product_sigma_finite "\<lambda>_. lborel"
     by standard
-  have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel)) 
+  have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
             ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) =
         nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
           (indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
           space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
     by (subst nn_integral_indicator) auto
-  also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> r} \<inter> 
-                                space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y)) 
+  also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> r} \<inter>
+                                space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y))
                    \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
     using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
-  also have "\<dots> = (\<integral>\<^sup>+ (y::real). \<integral>\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> 
+  also have "\<dots> = (\<integral>\<^sup>+ (y::real). \<integral>\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le>
                sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
   proof (intro nn_integral_cong, goal_cases)
     case (1 y f)
@@ -118,13 +115,13 @@
     thus ?case using 1 \<open>r > 0\<close>
       by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *)
   qed
-  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) 
+  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2))
                                    \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
                   \<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
-  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel)) 
+  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel))
       ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) \<partial>lborel)"
     using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
-  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) * 
+  also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) *
                                   (sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>lborel)"
   proof (intro nn_integral_cong_AE, goal_cases)
     case 1
@@ -141,28 +138,28 @@
       qed (insert elim, auto)
     qed
   qed
-  also have "\<dots> = ennreal (unit_ball_vol (real (card A))) * 
+  also have "\<dots> = ennreal (unit_ball_vol (real (card A))) *
                     (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)"
     by (subst nn_integral_cmult [symmetric])
        (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
   also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
-               (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
+               (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
                \<partial>(distr lborel borel ((*) (1/r))))" using \<open>r > 0\<close>
     by (subst nn_integral_distr)
        (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
-  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * 
+  also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
                (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
     by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
-  also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x * 
+  also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x *
                     sqrt (1 - x\<^sup>2) ^ card A \<partial>lborel)"
     by (subst nn_integral_cmult) auto
   also note emeasure_cball_aux_integral
   also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) *
-                 ennreal (Beta (1/2) (card A / 2 + 1))) = 
+                 ennreal (Beta (1/2) (card A / 2 + 1))) =
                ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))"
     using \<open>r > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
   also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))"
-    by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps 
+    by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps
           Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric])
   also have "Suc (card A) = card (insert i A)" using insert.hyps by simp
   finally show ?case .
@@ -182,11 +179,11 @@
 proof (cases "r = 0")
   case False
   with r have r: "r > 0" by simp
-  have "(lborel :: 'a measure) = 
+  have "(lborel :: 'a measure) =
           distr (Pi\<^sub>M Basis (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
     by (rule lborel_eq)
-  also have "emeasure \<dots> (cball 0 r) = 
-               emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel)) 
+  also have "emeasure \<dots> (cball 0 r) =
+               emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel))
                ({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
     by (subst emeasure_distr) (auto simp: cball_def)
   also have "{f. dist 0 (\<Sum>b\<in>Basis. f b *\<^sub>R b :: 'a) \<le> r} = {f. sqrt (\<Sum>i\<in>Basis. (f i)\<^sup>2) \<le> r}"
@@ -227,7 +224,7 @@
 
 
 text \<open>
-  Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in 
+  Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in
   the cases of even and odd integer dimensions.
 \<close>
 lemma unit_ball_vol_even:
@@ -240,7 +237,7 @@
         "unit_ball_vol (real (2 * n + 1)) =
            (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
 proof -
-  have "unit_ball_vol (real (2 * n + 1)) = 
+  have "unit_ball_vol (real (2 * n + 1)) =
           pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))"
     by (simp add: unit_ball_vol_def field_simps)
   also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)"
@@ -250,7 +247,7 @@
   also have "pi powr (real n + 1 / 2) / \<dots> = pi ^ n / pochhammer (1 / 2) (Suc n)"
     by (simp add: powr_add powr_half_sqrt powr_realpow)
   finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
-  also have "pochhammer (1 / 2 :: real) (Suc n) = 
+  also have "pochhammer (1 / 2 :: real) (Suc n) =
                fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))"
     using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac)
   also have "pi ^n / \<dots> = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
@@ -263,7 +260,7 @@
   "unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
     fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2)
 proof -
-  have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)" 
+  have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
     by (simp only: numeral_Bit0 mult_2 ring_distribs)
   also have "unit_ball_vol \<dots> = pi ^ numeral n / fact (numeral n)"
     by (rule unit_ball_vol_even)
diff -r e1b5bf983de3 -r aca96bd12b12 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Oct 04 15:01:50 2021 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Oct 04 16:11:18 2021 +0100
@@ -373,6 +373,17 @@
 lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
   unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
 
+lemma finite_inverse_image_gen:
+  assumes "finite A" "inj_on f D"
+  shows "finite {j\<in>D. f j \<in> A}"
+  using finite_vimage_IntI [OF assms]
+  by (simp add: Collect_conj_eq inf_commute vimage_def)
+
+lemma finite_inverse_image:
+  assumes "finite A" "inj f"
+  shows "finite {j. f j \<in> A}"
+  using finite_inverse_image_gen [OF assms] by simp
+
 lemma finite_Collect_bex [simp]:
   assumes "finite A"
   shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"
diff -r e1b5bf983de3 -r aca96bd12b12 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Oct 04 15:01:50 2021 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Oct 04 16:11:18 2021 +0100
@@ -1560,6 +1560,20 @@
   then show ?case by (force intro: mult_strict_mono' prod_nonneg)
 qed
 
+lemma prod_le_power:
+  assumes A: "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> n" "card A \<le> k" and "n \<ge> 1"
+  shows "prod f A \<le> n ^ k"
+  using A
+proof (induction A arbitrary: k rule: infinite_finite_induct)
+  case (insert i A)
+  then obtain k' where k': "card A \<le> k'" "k = Suc k'"
+    using Suc_le_D by force
+  have "f i * prod f A \<le> n * n ^ k'"
+    using insert \<open>n \<ge> 1\<close> k' by (intro prod_nonneg mult_mono; force)
+  then show ?case 
+    by (auto simp: \<open>k = Suc k'\<close> insert.hyps)
+qed (use \<open>n \<ge> 1\<close> in auto)
+
 end
 
 lemma prod_mono2:
diff -r e1b5bf983de3 -r aca96bd12b12 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Mon Oct 04 15:01:50 2021 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Mon Oct 04 16:11:18 2021 +0100
@@ -110,6 +110,25 @@
   using to_nat_on_infinite[of S, unfolded bij_betw_def]
   by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
 
+text \<open>
+  The sum/product over the enumeration of a finite set equals simply the sum/product over the set
+\<close>
+context comm_monoid_set
+begin
+
+lemma card_from_nat_into:
+  "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h A"
+proof (cases "finite A")
+  case True
+  have "F (\<lambda>i. h (from_nat_into A i)) {..<card A} = F h (from_nat_into A ` {..<card A})"
+    by (metis True bij_betw_def bij_betw_from_nat_into_finite reindex_cong)
+  also have "... = F h A"
+    by (metis True bij_betw_def bij_betw_from_nat_into_finite)
+  finally show ?thesis .
+qed auto
+
+end
+
 lemma countable_as_injective_image:
   assumes "countable A" "infinite A"
   obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f"
diff -r e1b5bf983de3 -r aca96bd12b12 src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Mon Oct 04 15:01:50 2021 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Mon Oct 04 16:11:18 2021 +0100
@@ -167,6 +167,20 @@
     by (intro disjointD[OF d]) auto
 qed
 
+lemma disjoint_family_on_iff_disjoint_image:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<noteq> {}"
+  shows "disjoint_family_on A I \<longleftrightarrow> disjoint (A ` I) \<and> inj_on A I"
+proof
+  assume "disjoint_family_on A I"
+  then show "disjoint (A ` I) \<and> inj_on A I"
+    by (metis (mono_tags, lifting) assms disjoint_family_onD disjoint_family_on_disjoint_image inf.idem inj_onI)
+qed (use disjoint_image_disjoint_family_on in metis)
+
+lemma card_UN_disjoint':
+  assumes "disjoint_family_on A I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "finite I"
+  shows "card (\<Union>i\<in>I. A i) = (\<Sum>i\<in>I. card (A i))"
+  using assms   by (simp add: card_UN_disjoint disjoint_family_on_def)
+
 lemma disjoint_UN:
   assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>(F i)) I"
   shows "disjoint (\<Union>i\<in>I. F i)"
@@ -217,6 +231,25 @@
   using disjoint_UN[of "{C, B}" "\<lambda>x. x"] by (auto simp add: disjoint_family_on_def)
 
 text \<open>
+  Sum/product of the union of a finite disjoint family
+\<close>
+context comm_monoid_set
+begin
+
+lemma UNION_disjoint_family:
+  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
+    and "disjoint_family_on A I"
+  shows "F g (\<Union>(A ` I)) = F (\<lambda>x. F g (A x)) I"
+  using assms unfolding disjoint_family_on_def  by (rule UNION_disjoint)
+
+lemma Union_disjoint_sets:
+  assumes "\<forall>A\<in>C. finite A" and "disjoint C"
+  shows "F g (\<Union>C) = (F \<circ> F) g C"
+  using assms unfolding disjoint_def  by (rule Union_disjoint)
+
+end
+
+text \<open>
   The union of an infinite disjoint family of non-empty sets is infinite.
 \<close>
 lemma infinite_disjoint_family_imp_infinite_UNION:
@@ -353,6 +386,11 @@
 lemma finite_elements: "finite A \<Longrightarrow> partition_on A P \<Longrightarrow> finite P"
   using partition_onD1[of A P] by (simp add: finite_UnionD)
 
+lemma product_partition:
+  assumes "partition_on A P" and "\<And>p. p \<in> P \<Longrightarrow> finite p" 
+  shows "card A = (\<Sum>p\<in>P. card p)"
+  using assms unfolding partition_on_def  by (meson card_Union_disjoint)
+
 subsection \<open>Equivalence of partitions and equivalence classes\<close>
 
 lemma partition_on_quotient:
diff -r e1b5bf983de3 -r aca96bd12b12 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Oct 04 15:01:50 2021 +0200
+++ b/src/HOL/Power.thy	Mon Oct 04 16:11:18 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