diff -r d1bd2144ab5d -r 9dd0274f76af src/HOL/Real/RealOrd.ML
--- a/src/HOL/Real/RealOrd.ML	Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML	Thu Jun 01 11:22:27 2000 +0200
@@ -1,7 +1,6 @@
 (*  Title:       HOL/Real/Real.ML
     ID:          $Id$
-    Author:      Lawrence C. Paulson
-                 Jacques D. Fleuriot
+    Author:      Jacques D. Fleuriot and Lawrence C. Paulson
     Copyright:   1998  University of Cambridge
     Description: Type "real" is a linear order
 *)
@@ -434,6 +433,26 @@
 
 Addsimps [real_mult_less_iff1,real_mult_less_iff2];
 
+(* 05/00 *)
+Goalw [real_le_def] "[| 0r<z; x*z<=y*z |] ==> x<=y";
+by (Auto_tac);
+qed "real_mult_le_cancel1";
+
+Goalw [real_le_def] "!!(x::real). [| 0r<z; z*x<=z*y |] ==> x<=y";
+by (Auto_tac);
+qed "real_mult_le_cancel2";
+
+Goalw [real_le_def] "0r < z ==> (x*z <= y*z) = (x <= y)";
+by (Auto_tac);
+qed "real_mult_le_cancel_iff1";
+
+Goalw [real_le_def] "0r < z ==> (z*x <= z*y) = (x <= y)";
+by (Auto_tac);
+qed "real_mult_le_cancel_iff2";
+
+Addsimps [real_mult_le_cancel_iff1,real_mult_le_cancel_iff2];
+
+
 Goal "[| 0r<=z; x<y |] ==> x*z<=y*z";
 by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
 by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
@@ -720,6 +739,34 @@
 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
 qed "real_rinv_add";
 
+(* 05/00 *)
+Goal "(0r <= -R) = (R <= 0r)";
+by (auto_tac (claset() addDs [sym],
+    simpset() addsimps [real_le_less]));
+qed "real_minus_zero_le_iff";
+
+Goal "(-R <= 0r) = (0r <= R)";
+by (auto_tac (claset(),simpset() addsimps 
+    [real_minus_zero_less_iff2,real_le_less]));
+qed "real_minus_zero_le_iff2";
+
+Goal "-(x*x) <= 0r";
+by (simp_tac (simpset() addsimps [real_minus_zero_le_iff2]) 1);
+qed "real_minus_squre_le_zero";
+Addsimps [real_minus_squre_le_zero];
+
+Goal "x * x + y * y = 0r ==> x = 0r";
+by (dtac real_add_minus_eq_minus 1);
+by (cut_inst_tac [("x","x")] real_le_square 1);
+by (Auto_tac THEN dtac real_le_anti_sym 1);
+by (auto_tac (claset() addDs [real_mult_zero_disj],simpset()));
+qed "real_sum_squares_cancel";
+
+Goal "x * x + y * y = 0r ==> y = 0r";
+by (res_inst_tac [("y","x")] real_sum_squares_cancel 1);
+by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
+qed "real_sum_squares_cancel2";
+
 (*----------------------------------------------------------------------------
      Another embedding of the naturals in the reals (see real_of_posnat)
  ----------------------------------------------------------------------------*)
@@ -780,3 +827,27 @@
 	      simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc, 
 				  real_of_nat_zero] @ real_add_ac));
 qed_spec_mp "real_of_nat_minus";
+
+(* 05/00 *)
+Goal "n2 < n1 ==> real_of_nat (n1 - n2) = \
+\     real_of_nat n1 + -real_of_nat n2";
+by (auto_tac (claset() addIs [real_of_nat_minus],simpset()));
+qed "real_of_nat_minus2";
+
+Goalw [real_diff_def] "n2 < n1 ==> real_of_nat (n1 - n2) = \
+\     real_of_nat n1 - real_of_nat n2";
+by (etac real_of_nat_minus2 1);
+qed "real_of_nat_diff";
+
+Goalw [real_diff_def] "n2 <= n1 ==> real_of_nat (n1 - n2) = \
+\     real_of_nat n1 - real_of_nat n2";
+by (etac real_of_nat_minus 1);
+qed "real_of_nat_diff2";
+
+Goal "(real_of_nat n ~= 0r) = (n ~= 0)";
+by (auto_tac (claset() addIs [inj_real_of_nat RS injD],
+    simpset() addsimps [real_of_nat_zero RS sym] 
+    delsimps [neq0_conv]));
+qed "real_of_nat_not_zero_iff";
+Addsimps [real_of_nat_not_zero_iff];
+