diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index fc7900a3a..2bb03d233 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -297,8 +297,6 @@ section field
   theorem div_div_div_div (Hb : b ≠ 0) (Hc : c ≠ 0) (Hd : d ≠ 0) : (a / b) / (c / d) = (a * d) / (b * c) :=
     by rewrite [(div_div_eq_mul_div Hc Hd), (div_mul_eq_mul_div), (div_div_eq_div_mul Hb Hc)]
 
-  -- remaining to transfer from Isabelle fields: ordered fields
-
 end field
 
 structure discrete_field [class] (A : Type) extends field A :=
diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean
index 876e35ccd..0d63ce211 100644
--- a/library/algebra/ordered_field.lean
+++ b/library/algebra/ordered_field.lean
@@ -297,6 +297,12 @@ section linear_ordered_field
       ... = (a * 2) / 2           : by rewrite left_distrib
       ... = a                     : by rewrite [@mul_div_cancel A _ _ _ two_ne_zero]
 
+  theorem sub_self_div_two : a - a / 2 = a / 2 :=
+    by rewrite [-{a}add_halves at {1}, add_sub_cancel]
+
+  theorem div_two_sub_self : a / 2 - a = - (a / 2) :=
+    by rewrite [-{a}add_halves at {2}, sub_add_eq_sub_sub, sub_self, zero_sub]
+
 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,