src/HOL/NthRoot.thy
changeset 31014 79f0858d9d49
parent 30273 ecd6f0ca62ea
child 31880 6fb86c61747c
     1.1 --- a/src/HOL/NthRoot.thy	Tue Apr 28 13:34:48 2009 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Tue Apr 28 15:50:29 2009 +0200
     1.3 @@ -565,16 +565,6 @@
     1.4  lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
     1.5  by (simp add: power2_eq_square [symmetric])
     1.6  
     1.7 -lemma power2_sum:
     1.8 -  fixes x y :: "'a::{number_ring,recpower}"
     1.9 -  shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
    1.10 -by (simp add: ring_distribs power2_eq_square)
    1.11 -
    1.12 -lemma power2_diff:
    1.13 -  fixes x y :: "'a::{number_ring,recpower}"
    1.14 -  shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
    1.15 -by (simp add: ring_distribs power2_eq_square)
    1.16 -
    1.17  lemma real_sqrt_sum_squares_triangle_ineq:
    1.18    "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
    1.19  apply (rule power2_le_imp_le, simp)