src/HOL/Real/RealDef.thy
changeset 22970 b5910e3dec4c
parent 22962 4bb05ba38939
child 23031 9da9585c816e
     1.1 --- a/src/HOL/Real/RealDef.thy	Mon May 14 18:04:52 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Mon May 14 18:48:24 2007 +0200
     1.3 @@ -557,18 +557,6 @@
     1.4  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
     1.5  by(simp add:mult_commute)
     1.6  
     1.7 -text{*FIXME: delete or at least combine the next two lemmas*}
     1.8 -lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
     1.9 -apply (drule OrderedGroup.equals_zero_I [THEN sym])
    1.10 -apply (cut_tac x = y in real_le_square) 
    1.11 -apply (auto, drule order_antisym, auto)
    1.12 -done
    1.13 -
    1.14 -lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
    1.15 -apply (rule_tac y = x in real_sum_squares_cancel)
    1.16 -apply (simp add: add_commute)
    1.17 -done
    1.18 -
    1.19  lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
    1.20  by (rule add_pos_pos)
    1.21  
    1.22 @@ -581,9 +569,6 @@
    1.23  lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
    1.24  by (simp add: one_less_inverse_iff)
    1.25  
    1.26 -lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
    1.27 -by (intro add_nonneg_nonneg zero_le_square)
    1.28 -
    1.29  
    1.30  subsection{*Embedding the Integers into the Reals*}
    1.31