diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 19a6721910..2b43d31fb9 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -21,15 +21,17 @@ local notation 1 := rat.of_num 1
 -------------------------------------
 -- theorems to add to (ordered) field and/or rat
 
-theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c :=
+-- this can move to pnat once sorry is filled in
+theorem find_midpoint {a b : ℚ} (H : a > b) : ∃ c : ℚ, a > b + c ∧ c > 0 :=
   exists.intro ((a - b) / (1 + 1))
-    (have H2 [visible] : a + a > (b + b) + (a - b), from calc
+    (and.intro (have H2 [visible] : a + a > (b + b) + (a - b), from calc
       a + a > b + a : rat.add_lt_add_right H
       ... = b + a + b - b : rat.add_sub_cancel
       ... = (b + b) + (a - b) : sorry, -- simp
      have H3 [visible] : (a + a) / (1 + 1) > ((b + b) + (a - b)) / (1 + 1),
        from div_lt_div_of_lt_of_pos H2 dec_trivial,
      by rewrite [div_two at H3, -div_add_div_same at H3, div_two at H3]; exact H3)
+    (pos_div_of_pos_of_pos (iff.mp' !sub_pos_iff_lt H) dec_trivial))
 
 theorem add_sub_comm (a b c d : ℚ) : a + b - (c + d) = (a - c) + (b - d) := sorry
 
@@ -47,7 +49,8 @@ theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0)
 -- small helper lemmas
 
 theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
-        p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ := sorry
+        p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ :=
+  by rewrite [rat.mul.assoc, rat.right_distrib, *inv_mul_eq_mul_inv]
 
 theorem find_thirds (a b : ℚ) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b := sorry
 
@@ -56,14 +59,22 @@ theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻
     apply rat.le_of_not_gt,
     intro Hb,
     apply (exists.elim (find_midpoint Hb)),
-    intros c Hc,
+    intro c Hc,
     apply (exists.elim (find_thirds b c)),
-    intros j Hbj,
-    have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj Hc,
+    intro j Hbj,
+    have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj (and.left Hc),
     exact absurd !H (not_le_of_gt Ha)
   end
 
-theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b := sorry
+theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b :=
+  begin
+    apply rat.le_of_not_gt,
+    intro Hb,
+    apply (exists.elim (find_midpoint Hb)),
+    intro c Hc,
+    let Hc' := H c (and.right Hc),
+    apply (rat.not_le_of_gt (and.left Hc)) ((iff.mp' !le_add_iff_sub_right_le) Hc')
+  end
 
 theorem rewrite_helper (a b c d : ℚ) : a * b  - c * d = a * (b - d) + (a - c) * d :=
   sorry
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index 91c384a06c..0df84670c6 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -12,11 +12,10 @@ and excluded middle.
 import data.real.basic data.real.order data.rat data.nat logic.axioms.classical
 open -[coercions] rat
 open -[coercions] nat
-local notation 0 := rat.of_num 0
-local notation 1 := rat.of_num 1
 open eq.ops pnat
 
-
+local notation 0 := rat.of_num 0
+local notation 1 := rat.of_num 1
 local notation 2 := pnat.pos (nat.of_num 2) dec_trivial
 
 namespace s
@@ -24,18 +23,13 @@ namespace s
 -----------------------------
 -- helper lemmas
 
-theorem abs_sub_square (a b : ℚ) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b :=
-  by rewrite [abs_mul_self, *rat.mul_sub_left_distrib, *rat.mul_sub_right_distrib,
-             sub_add_eq_sub_sub, sub_neg_eq_add, *rat.right_distrib, sub_add_eq_sub_sub, *one_mul,
-             *add.assoc, {_ + b * b}add.comm, {_ + (b * b + _)}add.comm, mul.comm b a, *add.assoc]
-
 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 rat.nonneg_le_nonneg_of_squares_le,
     repeat apply abs_nonneg,
-    rewrite [*(abs_sub_square _ _), *abs_abs, *abs_mul_self],
+    rewrite [*abs_sub_square, *abs_abs, *abs_mul_self],
     apply sub_le_sub_left,
     rewrite *rat.mul.assoc,
     apply rat.mul_le_mul_of_nonneg_left,
@@ -51,15 +45,11 @@ theorem forall_of_not_exists {A : Type} {P : A → Prop} (H : ¬ ∃ a : A, P a)
 theorem and_of_not_or {a b : Prop} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b :=
   and.intro (assume H', H (or.inl H')) (assume H', H (or.inr H'))
 
-theorem ne_zero_of_abs_ne_zero {a : ℚ} (H : abs a ≠ 0) : a ≠ 0 :=
-  assume Ha, H (Ha⁻¹ ▸ abs_zero)
-
 -----------------------------
 -- Facts about absolute values of sequences, to define inverse
 
 definition s_abs (s : seq) : seq := λ n, abs (s n)
 
-
 theorem abs_reg_of_reg {s : seq} (Hs : regular s) : regular (s_abs s) :=
   begin
     rewrite ↑regular at *,
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 1d5300870a..f49c06467e 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -17,20 +17,31 @@ open -[coercions] nat
 open eq eq.ops pnat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
+notation 2 := pnat.pos (of_num 2) dec_trivial
 
 ----------------------------------------------------------------------------------------------------
 
--- pnat theorems
-
-notation 2 := pnat.pos (of_num 2) dec_trivial
-
--- rat theorems
-theorem ge_sub_of_abs_sub_le_left {a b c : ℚ} (H : abs (a - b) ≤ c) : a ≥ b - c := sorry
-
-theorem ge_sub_of_abs_sub_le_right {a b c : ℚ} (H : abs (a - b) ≤ c) : b ≥ a - c :=
-  ge_sub_of_abs_sub_le_left (!abs_sub ▸ H)
-
-theorem sep_by_inv {a b : ℚ} (H : a > b) : ∃ N : ℕ+, a > (b + N⁻¹ + N⁻¹) := sorry
+-- this could be moved to pnat, but it uses find_midpoint which still has sorries in real.basic
+theorem sep_by_inv {a b : ℚ} (H : a > b) : ∃ N : ℕ+, a > (b + N⁻¹ + N⁻¹) :=
+  begin
+    apply exists.elim (find_midpoint H),
+    intro c Hc,
+    existsi (pceil ((1 + 1 + 1) / c)),
+    apply rat.lt.trans,
+    rotate 1,
+    apply and.left Hc,
+    rewrite rat.add.assoc,
+    apply rat.add_lt_add_left,
+    rewrite -(@rat.add_halves c) at {3},
+    apply rat.add_lt_add,
+    repeat (apply lt_of_le_of_lt;
+    apply inv_pceil_div;
+    apply dec_trivial;
+    apply and.right Hc;
+    apply div_lt_div_of_pos_of_lt_of_pos;
+    repeat (apply dec_trivial);
+    apply and.right Hc)
+  end
 
 theorem helper_1 {a : ℚ} (H : a > 0) : -a + -a ≤ -a := sorry
 
@@ -159,8 +170,8 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos
   end
 
 
-theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) (Hp : nonneg s) :
-       nonneg t :=
+theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t)
+        (Hp : nonneg s) : nonneg t :=
   begin
     apply nonneg_of_bdd_within,
     apply Ht,
@@ -342,11 +353,13 @@ theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonne
     apply Ht
   end
 
-theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Lst : s_le s t) (Ltu : s_le t u) : s_le s u :=
+theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) (Lst : s_le s t)
+        (Ltu : s_le t u) : s_le s u :=
   begin
     rewrite ↑s_le at *,
     let Rz := zero_is_reg,
-    have Hsum : nonneg (sadd (sadd u (sneg t)) (sadd t (sneg s))  ), from add_nonneg_of_nonneg Ltu Lst,
+    have Hsum : nonneg (sadd (sadd u (sneg t)) (sadd t (sneg s))),
+                from add_nonneg_of_nonneg Ltu Lst,
     have H' : nonneg (sadd (sadd u (sadd (sneg t) t)) (sneg s)), begin
       apply nonneg_of_nonneg_equiv,
       rotate 2,
@@ -384,7 +397,8 @@ theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u
     repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
   end
 
-theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_le s t) (Lts : s_le t s) : s ≡ t :=
+theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_le s t)
+        (Lts : s_le t s) : s ≡ t :=
   begin
     apply equiv_of_diff_equiv_zero,
     rotate 2,
@@ -411,7 +425,8 @@ theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s
 definition sep (s t : seq) := s_lt s t ∨ s_lt t s
 local infix `≢` : 50 := sep
 
-theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_lt s t) : s_le s t ∧ sep s t :=
+theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_lt s t) :
+        s_le s t ∧ sep s t :=
   begin
     apply and.intro,
     rewrite [↑s_lt at *, ↑pos at *, ↑s_le, ↑nonneg],
@@ -435,7 +450,8 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
     exact or.inl Lst
   end
 
-theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le s t ∧ sep s t) : s_lt s t :=
+theorem lt_of_le_and_sep {s t : seq} (Hs : regular s) (Ht : regular t) (H : s_le s t ∧ sep s t) :
+        s_lt s t :=
   begin
     let Le := and.left H,
     let Hsep := and.right H,
@@ -891,26 +907,6 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
   end
 
 
-
---------
--- These are currently needed for lin_ordered_comm_ring.
-
-/-theorem le_or_ge {s t : seq} (Hs : regular s) (Ht : regular t) : s_le s t ∨ s_le t s :=
-  sorry
-
-theorem lt_or_equiv_of_le {s t : seq} (Hs : regular s) (Ht : regular t) (Hle : s_le s t) :
-        s_lt s t ∨ s ≡ t :=
-  begin
-    apply sorry
-  end -- this is not constructive
-
-theorem le_iff_lt_or_equiv {s t : seq} (Hs : regular s) (Ht : regular t) :
-        s_le s t ↔ s_lt s t ∨ s ≡ t :=
-  iff.intro (lt_or_equiv_of_le Hs Ht) (le_of_lt_or_equiv Hs Ht)-/
-
-
-
-
 -------- lift to reg_seqs
 definition r_lt (s t : reg_seq) := s_lt (reg_seq.sq s) (reg_seq.sq t)
 definition r_le (s t : reg_seq) := s_le (reg_seq.sq s) (reg_seq.sq t)
@@ -986,15 +982,6 @@ theorem r_zero_lt_one : r_lt r_zero r_one := s_zero_lt_one
 theorem r_le_of_lt_or_eq (s t : reg_seq) (H : r_lt s t ∨ requiv s t) : r_le s t :=
   le_of_lt_or_equiv (reg_seq.is_reg s) (reg_seq.is_reg t) H
 
-----------
--- earlier versions are sorried
-/-theorem r_le_iff_lt_or_equiv (s t : reg_seq) : r_le s t ↔ r_lt s t ∨ requiv s t :=
-  le_iff_lt_or_equiv (reg_seq.is_reg s) (reg_seq.is_reg t)
-
-theorem r_le_or_ge (s t : reg_seq) : r_le s t ∨ r_le t s :=
-  le_or_ge (reg_seq.is_reg s) (reg_seq.is_reg t)-/
------------
-
 end s
 
 open real
@@ -1066,26 +1053,6 @@ theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
         apply (or.inr (quot.exact H'))
       end)))
 
-----------
--- earlier versions are sorried
-/-theorem le_iff_lt_or_eq (x y : ℝ) : x ≤ y ↔ x < y ∨ x = y :=
-  iff.intro
-    (quot.induction_on₂ x y (λ s t H, or.elim (iff.mp ((s.r_le_iff_lt_or_equiv s t)) H)
-      (take H1, or.inl H1)
-      (take H2, or.inr (quot.sound H2))))
-    (quot.induction_on₂ x y (λ s t H, or.elim H (take H', begin
-        let H'' := iff.mp' (s.r_le_iff_lt_or_equiv s t),
-        apply H'' (or.inl H')
-      end)
-      (take H', begin
-        let H'' := iff.mp' (s.r_le_iff_lt_or_equiv s t),
-        apply H'' (or.inr (quot.exact H'))
-      end)))
-
-theorem le_or_ge (x y : ℝ) : x ≤ y ∨ y ≤ x :=
-  quot.induction_on₂ x y (λ s t, s.r_le_or_ge s t)-/
--------------
-
 definition ordered_ring  : algebra.ordered_ring ℝ :=
   ⦃ algebra.ordered_ring, comm_ring,
     le_refl := le.refl,
@@ -1102,26 +1069,4 @@ definition ordered_ring  : algebra.ordered_ring ℝ :=
     add_lt_add_left := add_lt_add_left
   ⦄
 
------------------------------------
---- here is where classical logic comes in
---theorem sep_is_eq (x y : ℝ) : x ≢ y = ¬ (x = y) := sorry
-
-/-theorem sep_is_eq (x y : ℝ) : x ≢ y = ¬ (x = y) := begin
-   apply propext,
-   apply iff.intro,
-   intro Hsep,
-   intro Heq,
-   rewrite Heq at Hsep,
-   apply absurd Hsep !not_sep_self,
-   intro Hneq,
-  end-/
-
-/-definition linear_ordered_comm_ring : algebra.linear_ordered_comm_ring ℝ :=
-  ⦃ algebra.linear_ordered_comm_ring, ordered_ring, comm_ring,
-    zero_lt_one := zero_lt_one,
-    le_total := le_or_ge,
-    le_iff_lt_or_eq := le_iff_lt_or_eq
-  ⦄-/
-
-
 end real