chore(library/data/real): move more lemmas to algebra

library/algebra/ordered_field.lean

@@ -263,6 +263,17 @@ section linear_ordered_field
       ... = (a * (1 + 1)) / (1 + 1) : left_distrib
       ... = a : mul_div_cancel two_ne_zero
 
+theorem nonneg_le_nonneg_of_squares_le  (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a ≤ b * b) : a ≤ b :=
+  begin
+    apply le_of_not_gt,
+    intro Hab,
+    let Hposa := lt_of_le_of_lt Hb Hab,
+    let H' := calc
+      b * b ≤ a * b : mul_le_mul_of_nonneg_right (le_of_lt Hab) Hb
+      ... < a * a : mul_lt_mul_of_pos_left Hab Hposa,
+    apply (not_le_of_gt H') H
+  end
+
 end linear_ordered_field
 
 structure discrete_linear_ordered_field [class] (A : Type) extends linear_ordered_field A,

library/data/real/basic.lean

@@ -194,18 +194,6 @@ theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := so
 
 theorem div_helper (a b : ℚ) : (1 / (a * b)) * a = 1 / b := sorry
 
-theorem abs_add_three (a b c : ℚ) : abs (a + b + c) ≤ abs a + abs b + abs c := 
-  begin
-    apply rat.le.trans,
-    apply abs_add_le_abs_add_abs,
-    apply rat.add_le_add_right,
-    apply abs_add_le_abs_add_abs
-  end
-
-theorem add_le_add_three (a b c d e f : ℚ) (H1 : a ≤ d) (H2 : b ≤ e) (H3 : c ≤ f) :
-        a + b + c ≤ d + e + f :=
-  by repeat apply rat.add_le_add; repeat assumption
-
 theorem distrib_three_right (a b c d : ℚ) : (a + b + c) * d = a * d + b * d + c * d := sorry
 
 theorem mul_le_mul_of_mul_div_le (a b c d : ℚ) : a * (b / c) ≤ d → b * a ≤ d * c := sorry

library/data/real/division.lean

@@ -22,18 +22,6 @@ namespace s
 -----------------------------
 -- helper lemmas
 
-theorem nonneg_le_nonneg_of_squares_le {a b : ℚ} (Ha : a ≥ 0) (Hb : b ≥ 0) (H : a * a ≤ b * b) :
-        a ≤ b :=
-  begin
-    apply rat.le_of_not_gt,
-    intro Hab,
-    let Hposa := rat.lt_of_le_of_lt Hb Hab,
-    let H' := calc
-      b * b ≤ a * b : rat.mul_le_mul_of_nonneg_right (rat.le_of_lt Hab) Hb
-      ... < a * a : rat.mul_lt_mul_of_pos_left Hab Hposa,
-    apply (rat.not_le_of_gt H') H
-  end
-
 theorem abs_sub_square (a b : ℚ) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b := 
   sorry --begin rewrite [abs_mul_self, *rat.left_distrib, *rat.right_distrib, *one_mul] end
 
@@ -41,7 +29,7 @@ theorem neg_add_rewrite {a b : ℚ} : a + -b = -(b + -a) := sorry
 
 theorem abs_abs_sub_abs_le_abs_sub (a b : ℚ) : abs (abs a - abs b) ≤ abs (a - b) :=
   begin
-    apply nonneg_le_nonneg_of_squares_le,
+    apply rat.nonneg_le_nonneg_of_squares_le,
     repeat apply abs_nonneg,
     rewrite [*(abs_sub_square _ _), *abs_abs, *abs_mul_self],
     apply sub_le_sub_left,

library/data/real/order.lean

@@ -16,7 +16,6 @@ open -[coercions] rat
 open -[coercions] nat
 open eq eq.ops
  
-
 ----------------------------------------------------------------------------------------------------
 
 -- pnat theorems