diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean
index 3460fd2055..ab97100ce8 100644
--- a/library/data/int/gcd.lean
+++ b/library/data/int/gcd.lean
@@ -133,7 +133,7 @@ dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right
 theorem gcd_dvd_gcd_mul_right (a b c : ℤ) : gcd a b ∣ gcd (a * c) b :=
 !mul.comm ▸ !gcd_dvd_gcd_mul_left
 
-theorem div_gcd_eq_div_gcd_of_nonneg {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂)
+theorem div_gcd_eq_div_gcd_of_nonneg {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = a₂ * b₁)
     (H1 : b₁ ≠ 0) (H2 : b₂ ≠ 0) (H3 : a₁ ≥ 0) (H4 : a₂ ≥ 0) :
   a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) :=
 begin
@@ -142,24 +142,24 @@ begin
   intro H', apply H1, apply eq_zero_of_gcd_eq_zero_right H',
   intro H', apply H2, apply eq_zero_of_gcd_eq_zero_right H',
   rewrite [-abs_of_nonneg H3 at {1}, -abs_of_nonneg H4 at {2}],
-  rewrite [-gcd_mul_left, -gcd_mul_right, H]
+  rewrite [-gcd_mul_left, -gcd_mul_right, H, mul.comm b₁]
 end
 
-theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = b₁ * a₂) (H1 : b₁ > 0) (H2 : b₂ > 0) :
+theorem div_gcd_eq_div_gcd {a₁ b₁ a₂ b₂ : ℤ} (H : a₁ * b₂ = a₂ * b₁) (H1 : b₁ > 0) (H2 : b₂ > 0) :
   a₁ div (gcd a₁ b₁) = a₂ div (gcd a₂ b₂) :=
 or.elim (le_or_gt 0 a₁)
   (assume H3 : a₁ ≥ 0,
-    have H4 : b₁ * a₂ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2),
-    have H5 : a₂ ≥ 0, from nonneg_of_mul_nonneg_left H4 H1,
+    have H4 : a₂ * b₁ ≥ 0, by rewrite -H; apply mul_nonneg H3 (le_of_lt H2),
+    have H5 : a₂ ≥ 0, from nonneg_of_mul_nonneg_right H4 H1,
     div_gcd_eq_div_gcd_of_nonneg H (ne_of_gt H1) (ne_of_gt H2) H3 H5)
   (assume H3 : a₁ < 0,
-    have H4 : b₁ * a₂ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2,
-    assert H5 : a₂ < 0, from neg_of_mul_neg_left H4 (le_of_lt H1),
+    have H4 : a₂ * b₁ < 0, by rewrite -H; apply mul_neg_of_neg_of_pos H3 H2,
+    assert H5 : a₂ < 0, from neg_of_mul_neg_right H4 (le_of_lt H1),
     assert H6 : abs a₁ div (gcd (abs a₁) (abs b₁)) = abs a₂ div (gcd (abs a₂) (abs b₂)),
       begin
         apply div_gcd_eq_div_gcd_of_nonneg,
         rewrite [abs_of_pos H1, abs_of_pos H2, abs_of_neg H3, abs_of_neg H5],
-        rewrite [-neg_mul_eq_mul_neg, -neg_mul_eq_neg_mul, H],
+        rewrite [-*neg_mul_eq_neg_mul, H],
         apply ne_of_gt (abs_pos_of_pos H1),
         apply ne_of_gt (abs_pos_of_pos H2),
         repeat (apply abs_nonneg)
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 652e65e455..cd1ccd02e1 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -34,7 +34,6 @@ int.cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H)
 private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
 int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial)
 
-
 theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
 have H1 : b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹,
 have H2 : nonneg n, from true.intro,
@@ -299,6 +298,9 @@ theorem of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := trivial
 theorem of_nat_pos {n : ℕ} (Hpos : #nat n > 0) : of_nat n > 0 :=
 of_nat_lt_of_nat_of_lt Hpos
 
+theorem of_nat_succ_pos (n : nat) : of_nat (nat.succ n) > 0 :=
+of_nat_pos !nat.succ_pos
+
 theorem exists_eq_of_nat {a : ℤ} (H : 0 ≤ a) : ∃n : ℕ, a = of_nat n :=
 obtain (n : ℕ) (H1 : 0 + of_nat n = a), from le.elim H,
 exists.intro n (!zero_add ▸ (H1⁻¹))
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index a5bb9a3a57..f9930bf6e7 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -74,9 +74,6 @@ setoid.mk equiv equiv.is_equivalence
 
 /- field operations -/
 
-theorem of_nat_succ_pos (n : nat) : of_nat (nat.succ n) > 0 :=
-of_nat_pos !nat.succ_pos
-
 definition of_int (i : int) : prerat := prerat.mk i 1 !of_nat_succ_pos
 
 definition zero : prerat := of_int 0
@@ -104,6 +101,9 @@ theorem of_int_mul (a b : ℤ) : of_int (#int a * b) ≡ mul (of_int a) (of_int
 theorem of_int_neg (a : ℤ) : of_int (#int -a) ≡ neg (of_int a) :=
 !equiv.refl
 
+theorem of_int.inj {a b : ℤ} : of_int a ≡ of_int b → a = b :=
+by rewrite [↑of_int, ↑equiv, *mul_one]; intros; assumption
+
 definition inv : prerat → prerat
 | inv (prerat.mk nat.zero d dp) := zero
 | inv (prerat.mk (nat.succ n) d dp) := prerat.mk d (nat.succ n) !of_nat_succ_pos
@@ -261,6 +261,64 @@ begin
   exact zero_ne_one
 end
 
+theorem mul_denom_equiv (a : prerat) : mul a (of_int (denom a)) ≡ of_int (num a) :=
+by esimp [mul, of_int, equiv]; rewrite [*int.mul_one]
+
+/- Reducing a fraction to lowest terms. Needed to choose a canonical representative of rat, and
+   define numerator and denominator. -/
+
+definition reduce : prerat → prerat
+| (mk an ad adpos) :=
+    have pos : ad div gcd an ad > 0, from div_pos_of_pos_of_dvd adpos !gcd_nonneg !gcd_dvd_right,
+    if an = 0 then prerat.zero
+              else mk (an div gcd an ad) (ad div gcd an ad) pos
+
+protected theorem eq {a b : prerat} (Hn : num a = num b) (Hd : denom a = denom b) : a = b :=
+begin
+  cases a with [an, ad, adpos],
+  cases b with [bn, bd, bdpos],
+  generalize adpos, generalize bdpos,
+  esimp at *,
+  rewrite [Hn, Hd],
+  intros, apply rfl
+end
+
+theorem reduce_equiv : ∀ a : prerat, reduce a ≡ a
+| (mk an ad adpos) :=
+    decidable.by_cases
+      (assume anz : an = 0,
+        by krewrite [↑reduce, if_pos anz, ↑equiv, anz, *zero_mul])
+      (assume annz : an ≠ 0,
+        by rewrite [↑reduce, if_neg annz, ↑equiv, int.mul.comm, -!mul_div_assoc !gcd_dvd_left,
+                       -!mul_div_assoc !gcd_dvd_right, int.mul.comm])
+
+theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b
+| (mk an ad adpos) (mk bn bd bdpos) :=
+  assume H : an * bd = bn * ad,
+  decidable.by_cases
+    (assume anz : an = 0,
+      have H' : bn * ad = 0, by rewrite [-H, anz, zero_mul],
+      assert bnz : bn = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt adpos),
+      by rewrite [↑reduce, if_pos anz, if_pos bnz])
+    (assume annz : an ≠ 0,
+      assert bnnz : bn ≠ 0, from
+        assume bnz,
+        have H' : an * bd = 0, by rewrite [H, bnz, zero_mul],
+        have anz : an = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H') (ne_of_gt bdpos),
+        show false, from annz anz,
+      begin
+        rewrite [↑reduce, if_neg annz, if_neg bnnz],
+        apply prerat.eq,
+          {apply div_gcd_eq_div_gcd H adpos bdpos},
+          {esimp, rewrite [gcd.comm, gcd.comm bn],
+            apply div_gcd_eq_div_gcd_of_nonneg,
+              rewrite [int.mul.comm, -H, int.mul.comm],
+              apply annz,
+              apply bnnz,
+              apply le_of_lt adpos,
+              apply le_of_lt bdpos},
+      end)
+
 end prerat
 
 /-
@@ -276,46 +334,49 @@ namespace rat
 
 /- operations -/
 
--- these coercions do not work: rat is not an inductive type
 definition of_int [coercion] (i : ℤ) : ℚ := ⟦prerat.of_int i⟧
 definition of_nat [coercion] (n : ℕ) : ℚ := ⟦prerat.of_int n⟧
 definition of_num [coercion] [reducible] (n : num) : ℚ := of_int (int.of_num n)
 
 definition add : ℚ → ℚ → ℚ :=
 quot.lift₂
-  (λa b : prerat, ⟦prerat.add a b⟧)
+  (λ a b : prerat, ⟦prerat.add a b⟧)
   (take a1 a2 b1 b2, assume H1 H2, quot.sound (prerat.add_equiv_add H1 H2))
 
 definition mul : ℚ → ℚ → ℚ :=
 quot.lift₂
-  (λa b : prerat, ⟦prerat.mul a b⟧)
+  (λ a b : prerat, ⟦prerat.mul a b⟧)
   (take a1 a2 b1 b2, assume H1 H2, quot.sound (prerat.mul_equiv_mul H1 H2))
 
 definition neg : ℚ → ℚ :=
 quot.lift
-  (λa : prerat, ⟦prerat.neg a⟧)
+  (λ a : prerat, ⟦prerat.neg a⟧)
   (take a1 a2, assume H, quot.sound (prerat.neg_equiv_neg H))
 
 definition inv : ℚ → ℚ :=
 quot.lift
-  (λa : prerat, ⟦prerat.inv a⟧)
+  (λ a : prerat, ⟦prerat.inv a⟧)
   (take a1 a2, assume H, quot.sound (prerat.inv_equiv_inv H))
 
-definition zero := ⟦prerat.zero⟧
-definition one := ⟦prerat.one⟧
+definition reduce : ℚ → prerat :=
+quot.lift
+  (λ a : prerat, prerat.reduce a)
+  @prerat.reduce_eq_reduce
 
-infix `+`    := rat.add
-infix `*`    := rat.mul
-prefix `-`   := rat.neg
-postfix `⁻¹` := rat.inv
+definition num (a : ℚ) : ℤ := prerat.num (reduce a)
+definition denom (a : ℚ) : ℤ := prerat.denom (reduce a)
+
+theorem denom_pos (a : ℚ): denom a > 0 :=
+prerat.denom_pos (reduce a)
+
+infix +    := rat.add
+infix *    := rat.mul
+prefix -   := rat.neg
 
 definition sub [reducible] (a b : rat) : rat := a + (-b)
 
-infix `-`    := rat.sub
-
--- TODO: this is a workaround, since the coercions from numerals do not work
-notation 0 := zero
-notation 1 := one
+postfix ⁻¹ := rat.inv
+infix -    := rat.sub
 
 /- properties -/
 
@@ -333,6 +394,9 @@ calc
   of_int (#int a - b) = of_int a + of_int (#int -b) : of_int_add
                   ... = of_int a - of_int b         : {of_int_neg b}
 
+theorem of_int.inj {a b : ℤ} (H : of_int a = of_int b) : a = b :=
+sorry
+
 theorem of_nat_eq (a : ℕ) : of_nat a = of_int (int.of_nat a) := rfl
 
 theorem of_nat_add (a b : ℕ) : of_nat (#nat a + b) = of_nat a + of_nat b :=
@@ -384,7 +448,7 @@ quot.induction_on a
 theorem inv_mul_cancel {a : ℚ} (H : a ≠ 0) : a⁻¹ * a = 1 :=
 !mul.comm ▸ mul_inv_cancel H
 
-theorem zero_ne_one : (#rat 0 ≠ 1) :=
+theorem zero_ne_one : (0 : ℚ) ≠ 1 :=
 assume H, prerat.zero_not_equiv_one (quot.exact H)
 
 definition has_decidable_eq [instance] : decidable_eq ℚ :=
@@ -397,6 +461,13 @@ take a b, quot.rec_on_subsingleton₂ a b
 theorem inv_zero : inv 0 = 0 :=
 quot.sound (prerat.inv_zero' ▸ !prerat.equiv.refl)
 
+theorem quot_reduce (a : ℚ) : ⟦reduce a⟧ = a :=
+quot.induction_on a (take u, quot.sound !prerat.reduce_equiv)
+
+theorem mul_denom (a : ℚ) : a * denom a = num a :=
+have H : ⟦reduce a⟧ * of_int (denom a) = of_int (num a), from quot.sound (!prerat.mul_denom_equiv),
+quot_reduce a ▸ H
+
 section migrate_algebra
   open [classes] algebra
 
@@ -433,4 +504,21 @@ section migrate_algebra
     replacing sub → rat.sub, divide → divide, dvd → dvd
 
 end migrate_algebra
+
+theorem eq_num_div_denom (a : ℚ) : a = num a / denom a :=
+have H : of_int (denom a) ≠ 0, from assume H', ne_of_gt (denom_pos a) (of_int.inj H'),
+iff.mp' (eq_div_iff_mul_eq H) (mul_denom a)
+
+theorem of_nat_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b :=
+decidable.by_cases
+  (assume bz : b = 0,
+    by rewrite [bz, div_zero, int.div_zero])
+  (assume bnz : b ≠ 0,
+    have bnz' : of_int b ≠ 0, from assume oibz, bnz (of_int.inj oibz),
+    have H' : of_int (a div b) * of_int b = of_int a, from
+      int.dvd.elim H
+        (take c, assume Hc : a = b * c,
+          by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]),
+    iff.mp' (eq_div_iff_mul_eq bnz') H')
+
 end rat
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 8bdb3dab7f..42b757309f 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -10,7 +10,7 @@ import data.int algebra.ordered_field .basic
 open quot eq.ops
 
 /- the ordering on representations -/
- 
+
 namespace prerat
 section int_notation
 open int
@@ -126,7 +126,7 @@ private theorem pos_of_nonneg_of_ne_zero : nonneg a → ¬ a = 0 → pos a :=
 quot.induction_on a
   (take u,
     assume H1 : nonneg ⟦u⟧,
-    assume H2 : ⟦u⟧ ≠ 0,
+    assume H2 : ⟦u⟧ ≠ (rat.of_num 0),
     have H3 : ¬ (prerat.equiv u prerat.zero), from assume H, H2 (quot.sound H),
     prerat.pos_of_nonneg_of_ne_zero H1 H3)
 
@@ -204,7 +204,7 @@ or.elim (nonneg_total (b - a))
   (assume H, or.inl H)
   (assume H, or.inr (!neg_sub ▸ H))
 
-theorem le.by_cases {P : Prop} (a b : ℚ) (H : a ≤ b → P) (H2 : b ≤ a → P) : P := 
+theorem le.by_cases {P : Prop} (a b : ℚ) (H : a ≤ b → P) (H2 : b ≤ a → P) : P :=
   or.elim (!rat.le.total) H H2
 
 theorem lt_iff_le_and_ne (a b : ℚ) : a < b ↔ a ≤ b ∧ a ≠ b :=
@@ -229,16 +229,16 @@ iff.intro
       (assume H1 : a < b, and.left (iff.mp !lt_iff_le_and_ne H1))
       (assume H1 : a = b, H1 ▸ !le.refl))
 
-theorem add_le_add_left (H : a ≤ b) (c: ℚ) : c + a ≤ c + b :=
+theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b :=
 have H1 : c + b - (c + a) = b - a,
   by rewrite [↑sub, neg_add, -add.assoc, add.comm c, add_neg_cancel_right],
 show nonneg (c + b - (c + a)), from H1⁻¹ ▸ H
 
-theorem mul_nonneg (H1 : a ≥ 0) (H2 : b ≥ 0) : a * b ≥ 0 :=
+theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 : ℚ) :=
 have H : nonneg (a * b), from nonneg_mul (!sub_zero ▸ H1) (!sub_zero ▸ H2),
 !sub_zero⁻¹ ▸ H
 
-theorem mul_pos (H1 : a > 0) (H2 : b > 0) : a * b > 0 :=
+theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
 have H : pos (a * b), from pos_mul (!sub_zero ▸ H1) (!sub_zero ▸ H2),
 !sub_zero⁻¹ ▸ H
 
@@ -247,17 +247,17 @@ take a b, decidable_pos (b - a)
 
 theorem le_of_lt  (H : a < b) : a ≤ b := iff.mp' !le_iff_lt_or_eq (or.inl H)
 
-theorem lt_irrefl (a : ℚ) : ¬ a < a := 
+theorem lt_irrefl (a : ℚ) : ¬ a < a :=
   take Ha,
-  let Hand := (iff.mp !lt_iff_le_and_ne) Ha in 
+  let Hand := (iff.mp !lt_iff_le_and_ne) Ha in
   (and.right Hand) rfl
 
 theorem not_le_of_gt (H : a < b) : ¬ b ≤ a :=
   assume Hba,
-  let Heq := le.antisymm (le_of_lt H) Hba in 
-  !lt_irrefl (Heq ▸ H) 
+  let Heq := le.antisymm (le_of_lt H) Hba in
+  !lt_irrefl (Heq ▸ H)
 
-theorem lt_of_lt_of_le  (Hab : a < b) (Hbc : b ≤ c) : a < c := 
+theorem lt_of_lt_of_le  (Hab : a < b) (Hbc : b ≤ c) : a < c :=
   let Hab' := le_of_lt Hab in
   let Hac := le.trans Hab' Hbc in
   (iff.mp' !lt_iff_le_and_ne) (and.intro Hac
@@ -275,8 +275,8 @@ theorem zero_lt_one : (0 : ℚ) < 1 := trivial
 --    apply sorry
 --  end
 
-theorem add_lt_add_left (H : a < b) (c : ℚ) : c + a < c + b := 
-let H' := le_of_lt H in 
+theorem add_lt_add_left (H : a < b) (c : ℚ) : c + a < c + b :=
+let H' := le_of_lt H in
 (iff.mp' (lt_iff_le_and_ne _ _)) (and.intro (add_le_add_left H' _)
                                   (take Heq, let Heq' := add_left_cancel Heq in
                                    !lt_irrefl (Heq' ▸ H)))
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index a684641c9a..53f32d2dd6 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -14,6 +14,8 @@ To do:
 import data.nat data.rat.order
 open nat eq eq.ops
 open -[coercions] rat
+local notation 0 := rat.of_num 0
+local notation 1 := rat.of_num 1
 ----------------------------------------------------------------------------------------------------
 
 -----------------------------------------------
@@ -730,7 +732,7 @@ theorem neg_s_cancel (s : seq) (H : regular s) : sadd s (sneg s) ≡ zero :=
     apply zero_is_reg
   end
 
-theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) 
+theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
         (Hv : regular v) (Esu : s ≡ u) (Etv : t ≡ v) : sadd s t ≡ sadd u v :=
   begin
     rewrite [↑sadd, ↑equiv at *],
@@ -1070,7 +1072,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
       pone⁻¹ = 1 : by rewrite -pone_inv
       ... = abs 1 : abs_of_pos zero_lt_one
       ... ≤ 2⁻¹ : H,
-    let H'' := ge_of_inv_le H', 
+    let H'' := ge_of_inv_le H',
     apply absurd (one_lt_two) (pnat.not_lt_of_le (pnat.le_of_lt H''))
   end
 
@@ -1155,7 +1157,7 @@ theorem r_distrib (s t u : reg_seq) : requiv (s * (t + u)) (s * t + s * u) :=
   s_distrib (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u)
 
 theorem r_zero_nequiv_one : ¬ requiv r_zero r_one :=
-  zero_nequiv_one 
+  zero_nequiv_one
 
 ----------------------------------------------
 -- take quotients to get ℝ and show it's a comm ring
@@ -1219,7 +1221,7 @@ theorem distrib (x y z : ℝ) : x * (y + z) = x * y + x * z :=
 theorem distrib_l (x y z : ℝ) : (x + y) * z = x * z + y * z :=
   by rewrite [mul_comm, distrib, {x * _}mul_comm, {y * _}mul_comm] -- this shouldn't be necessary
 
-theorem zero_ne_one : ¬ zero = one := 
+theorem zero_ne_one : ¬ zero = one :=
   take H : zero = one,
   absurd (quot.exact H) (r_zero_nequiv_one)
 
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index fee59d248f..78ead4b03f 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -10,9 +10,11 @@ At this point, we no longer proceed constructively: this file makes heavy use of
 
 Here, we show that ℝ is complete.
 -/
- 
+
 import data.real.basic data.real.order data.real.division data.rat data.nat logic.axioms.classical
-open -[coercions] rat 
+open -[coercions] rat
+local notation 0 := rat.of_num 0
+local notation 1 := rat.of_num 1
 open -[coercions] nat
 open algebra
 open eq.ops
@@ -36,7 +38,7 @@ theorem const_reg (a : ℚ) : regular (const a) :=
 
 definition r_const (a : ℚ) : reg_seq := reg_seq.mk (const a) (const_reg a)
 
-theorem rat_approx_l1 {s : seq} (H : regular s) : 
+theorem rat_approx_l1 {s : seq} (H : regular s) :
         ∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ :=
   begin
     intro n,
@@ -50,8 +52,8 @@ theorem rat_approx_l1 {s : seq} (H : regular s) :
     apply inv_ge_of_le Hm
   end
 
-theorem rat_approx {s : seq} (H : regular s) : 
-        ∀ n : ℕ+, ∃ q : ℚ, s_le (s_abs (sadd s (sneg (const q)))) (const n⁻¹) := 
+theorem rat_approx {s : seq} (H : regular s) :
+        ∀ n : ℕ+, ∃ q : ℚ, s_le (s_abs (sadd s (sneg (const q)))) (const n⁻¹) :=
   begin
     intro m,
     rewrite ↑s_le,
@@ -81,11 +83,11 @@ theorem rat_approx {s : seq} (H : regular s) :
     apply inv_pos
   end
 
-definition r_abs (s : reg_seq) : reg_seq := 
+definition r_abs (s : reg_seq) : reg_seq :=
   reg_seq.mk (s_abs (reg_seq.sq s)) (abs_reg_of_reg (reg_seq.is_reg s))
 
 theorem abs_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) :
-        s_abs s ≡ s_abs t := 
+        s_abs s ≡ s_abs t :=
   begin
     rewrite [↑equiv at *],
     intro n,
@@ -95,11 +97,11 @@ theorem abs_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s
     apply Heq
   end
 
-theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (r_abs t) := 
+theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (r_abs t) :=
   abs_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) H
 
 theorem r_rat_approx (s : reg_seq) :
-        ∀ n : ℕ+, ∃ q : ℚ, r_le (r_abs (radd s (rneg (r_const q)))) (r_const n⁻¹) := 
+        ∀ n : ℕ+, ∃ q : ℚ, r_le (r_abs (radd s (rneg (r_const q)))) (r_const n⁻¹) :=
   rat_approx (reg_seq.is_reg s)
 
 theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) : s_le (s_abs (sadd s (sneg (const (s n))))) (const n⁻¹) :=
@@ -123,7 +125,7 @@ theorem abs_const (a : ℚ) : const (abs a) ≡ s_abs (const a) :=
 
 theorem r_abs_const (a : ℚ) : requiv (r_const (abs a) ) (r_abs (r_const a)) := abs_const a
 
-theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) := 
+theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) :=
   begin
     rewrite [↑sadd, ↑const],
     apply equiv.refl
@@ -158,7 +160,7 @@ theorem r_le_of_const_le_const {a b : ℚ} (H : r_le (r_const a) (r_const b)) :
   le_of_const_le_const H
 
 theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_abs s ≡ s :=
-  begin 
+  begin
     apply eq_of_bdd,
     apply abs_reg_of_reg Hs,
     apply Hs,
@@ -174,7 +176,7 @@ theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_a
     apply inv_pos,
     intro Hneg,
     let Hneg' := lt_of_not_ge Hneg,
-    have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'), 
+    have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'),
     rewrite [rat.abs_of_neg Hneg', rat.abs_of_pos Hsn],
     apply rat.le.trans,
     apply rat.add_le_add,
@@ -220,13 +222,13 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) :
     intro Hneg,
     let Hneg' := lt_of_not_ge Hneg,
     rewrite [rat.abs_of_neg Hneg', ↑sneg, rat.sub_neg_eq_add, rat.neg_add_eq_sub, rat.sub_self,
-                abs_zero], 
+                abs_zero],
     apply rat.le_of_lt,
     apply inv_pos
   end
 
 theorem r_equiv_abs_of_ge_zero {s : reg_seq} (Hz : r_le r_zero s) : requiv (r_abs s) s :=
-  equiv_abs_of_ge_zero (reg_seq.is_reg s) Hz 
+  equiv_abs_of_ge_zero (reg_seq.is_reg s) Hz
 
 theorem r_equiv_neg_abs_of_le_zero {s : reg_seq} (Hz : r_le s r_zero) : requiv (r_abs s) (-s) :=
   equiv_neg_abs_of_le_zero (reg_seq.is_reg s) Hz
@@ -241,23 +243,23 @@ theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :
 
 definition rep (x : ℝ) : reg_seq := some (quot.exists_rep x)
 
-definition const (a : ℚ) : ℝ := quot.mk (s.r_const a) 
+definition const (a : ℚ) : ℝ := quot.mk (s.r_const a)
 
-theorem add_consts (a b : ℚ) : const a + const b = const (a + b) := 
+theorem add_consts (a b : ℚ) : const a + const b = const (a + b) :=
   quot.sound (s.r_add_consts a b)
 
 theorem sub_consts (a b : ℚ) : const a - const b = const (a - b) := !add_consts
 
-theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := 
+theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) :=
   by rewrite [add_consts, padd_halves]
 
-theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b := 
+theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b :=
   s.r_const_le_const_of_le
 
-theorem le_of_const_le_const (a b : ℚ) : const a ≤ const b → a ≤ b := 
+theorem le_of_const_le_const (a b : ℚ) : const a ≤ const b → a ≤ b :=
   s.r_le_of_const_le_const
 
-definition re_abs (x : ℝ) : ℝ := 
+definition re_abs (x : ℝ) : ℝ :=
   quot.lift_on x (λ a, quot.mk (s.r_abs a)) (take a b Hab, quot.sound (s.r_abs_well_defined Hab))
 
 theorem r_abs_nonneg {x : ℝ} : 0 ≤ x → re_abs x = x :=
@@ -293,7 +295,7 @@ theorem rat_approx (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, abs (x - const q) ≤
 
 definition approx (x : ℝ) (n : ℕ+) := some (rat_approx x n)
 
-theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (const (approx x n))) ≤ const n⁻¹ := 
+theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (const (approx x n))) ≤ const n⁻¹ :=
   some_spec (rat_approx x n)
 
 theorem approx_spec' (x : ℝ) (n : ℕ+) : abs ((const (approx x n)) - x) ≤ const n⁻¹ :=
@@ -310,7 +312,7 @@ definition cauchy (X : r_seq) (M : ℕ+ → ℕ+) :=
 theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : converges_to X a N) :
         cauchy X (λ k, N (2 * k)) :=
   begin
-    intro k m n Hm Hn, 
+    intro k m n Hm Hn,
     rewrite (rewrite_helper9 a),
     apply algebra.le.trans,
     apply algebra.abs_add_le_abs_add_abs,
@@ -334,13 +336,13 @@ theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !max_l
 definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : seq :=
   λ k, approx (X (Nb M k)) (2 * k)
 
-theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+} 
+theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+}
         (Hmn : M (2 * n) ≤M (2 * m)) :
            abs (const (lim_seq Hc m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs
             (X (Nb M n) - const (lim_seq Hc n)) ≤ const (m⁻¹ + n⁻¹) :=
   begin
     apply algebra.le.trans,
-    apply algebra.add_le_add_three, 
+    apply algebra.add_le_add_three,
     apply approx_spec',
     rotate 1,
     apply approx_spec,
@@ -359,14 +361,14 @@ theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m
     apply pnat.mul_le_mul_left
   end
 
-theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular (lim_seq Hc) := 
+theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular (lim_seq Hc) :=
   begin
     rewrite ↑regular,
     intro m n,
     apply le_of_const_le_const,
     rewrite [abs_const, -sub_consts, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
     apply algebra.le.trans,
-    apply algebra.abs_add_three, 
+    apply algebra.abs_add_three,
     let Hor := decidable.em (M (2 * m) ≥ M (2 * n)),
     apply or.elim Hor,
     intro Hor1,
@@ -378,7 +380,7 @@ theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular
     apply lim_seq_reg_helper Hc Hor2'
   end
 
-theorem lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) : 
+theorem lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) :
         s.s_le (s.s_abs (sadd (lim_seq Hc) (sneg (s.const (lim_seq Hc k))) )) (s.const k⁻¹) :=
   begin
     apply s.const_bound,
@@ -389,26 +391,26 @@ definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : reg_seq
   reg_seq.mk (lim_seq Hc) (lim_seq_reg Hc)
 
 theorem r_lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) :
-        s.r_le (s.r_abs (((r_lim_seq Hc) + -s.r_const ((reg_seq.sq (r_lim_seq Hc)) k)))) (s.r_const (k)⁻¹) := 
+        s.r_le (s.r_abs (((r_lim_seq Hc) + -s.r_const ((reg_seq.sq (r_lim_seq Hc)) k)))) (s.r_const (k)⁻¹) :=
   lim_seq_spec Hc k
 
 definition lim {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℝ :=
   quot.mk (r_lim_seq Hc)
 
-theorem re_lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : 
+theorem re_lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
         re_abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
-  r_lim_seq_spec Hc k 
+  r_lim_seq_spec Hc k
 
-theorem lim_spec' {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : 
+theorem lim_spec' {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
         abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
   by rewrite -re_abs_is_abs; apply re_lim_spec
 
-theorem lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : 
+theorem lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
         abs ((const ((lim_seq Hc) k)) - (lim Hc)) ≤ const (k)⁻¹ :=
   by rewrite algebra.abs_sub; apply lim_spec'
 
-theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : 
-        converges_to X (lim Hc) (Nb M) := 
+theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) :
+        converges_to X (lim Hc) (Nb M) :=
   begin
     intro k n Hn,
     rewrite (rewrite_helper10 (X (Nb M n)) (const (lim_seq Hc n))),
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index 63c7f11b34..a52003ed35 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -10,8 +10,10 @@ and excluded middle.
 -/
 
 import data.real.basic data.real.order data.rat data.nat logic.axioms.classical
-open -[coercions] rat 
+open -[coercions] rat
 open -[coercions] nat
+local notation 0 := rat.of_num 0
+local notation 1 := rat.of_num 1
 open eq.ops
 
 
@@ -22,7 +24,7 @@ namespace s
 -----------------------------
 -- helper lemmas
 
-theorem abs_sub_square (a b : ℚ) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b := 
+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
 
 theorem neg_add_rewrite {a b : ℚ} : a + -b = -(b + -a) := sorry
@@ -50,10 +52,10 @@ theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (pnat.to_rat n * pnat.to_
 theorem forall_of_not_exists {A : Type} {P : A → Prop} (H : ¬ ∃ a : A, P a) : ∀ a : A, ¬ P a :=
   take a, assume Ha, H (exists.intro a Ha)
 
-theorem and_of_not_or {a b : Prop} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b := 
+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 := 
+theorem ne_zero_of_abs_ne_zero {a : ℚ} (H : abs a ≠ 0) : a ≠ 0 :=
   assume Ha, H (Ha⁻¹ ▸ abs_zero)
 
 -----------------------------
@@ -162,17 +164,17 @@ theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : 
     apply dif_neg (pnat.not_lt_of_le Hn)
   end
 
-theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+} 
+theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
         (Hn : n < (pb Hs Hpos)) : s_inv Hs n = 1 / s ((pb Hs Hpos) * (pb Hs Hpos) * (pb Hs Hpos)) :=
   s_inv_of_sep_lt_p Hs (sep_zero_of_pos Hs Hpos) Hn
 
 
-theorem s_inv_of_pos_gt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+} 
+theorem s_inv_of_pos_gt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
         (Hn : n ≥ (pb Hs Hpos)) : s_inv Hs n = 1 / s ((pb Hs Hpos) * (pb Hs Hpos) * n) :=
   s_inv_of_sep_gt_p Hs (sep_zero_of_pos Hs Hpos) Hn
 
 theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) :
-        abs (s_inv Hs n) ≤ (pnat.to_rat (ps Hs Hsep)) := 
+        abs (s_inv Hs n) ≤ (pnat.to_rat (ps Hs Hsep)) :=
   if Hn : n < ps Hs Hsep then
     (begin
       rewrite [(s_inv_of_sep_lt_p Hs Hsep Hn), abs_one_div],
@@ -202,7 +204,7 @@ theorem s_inv_of_zero {s : seq} (Hs : regular s) (Hz : ¬ sep s zero) : s_inv Hs
     apply s_inv_of_zero' Hs Hz n
   end
 
-theorem s_ne_zero_of_ge_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+} 
+theorem s_ne_zero_of_ge_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
         (Hn : n ≥ (ps Hs Hsep)) : s n ≠ 0 :=
   begin
     let Hps := ps_spec Hs Hsep,
@@ -218,12 +220,12 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
   begin
     rewrite ↑regular,
     intros,
-    have Hsp : s ((ps Hs Hsep) * (ps Hs Hsep) * (ps Hs Hsep)) ≠ 0, from 
+    have Hsp : s ((ps Hs Hsep) * (ps Hs Hsep) * (ps Hs Hsep)) ≠ 0, from
       s_ne_zero_of_ge_p Hs Hsep !pnat.mul_le_mul_left,
-    have Hspn : s ((ps Hs Hsep) * (ps Hs Hsep) * n) ≠ 0, from 
+    have Hspn : s ((ps Hs Hsep) * (ps Hs Hsep) * n) ≠ 0, from
       s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * n ≥ ps Hs Hsep, by
         rewrite pnat_mul_assoc; apply pnat.mul_le_mul_right),
-    have Hspm : s ((ps Hs Hsep) * (ps Hs Hsep) * m) ≠ 0, from 
+    have Hspm : s ((ps Hs Hsep) * (ps Hs Hsep) * m) ≠ 0, from
       s_ne_zero_of_ge_p Hs Hsep (show (ps Hs Hsep) * (ps Hs Hsep) * m ≥ ps Hs Hsep, by
         rewrite pnat_mul_assoc; apply pnat.mul_le_mul_right),
     apply @decidable.cases_on (m < (ps Hs Hsep)) _ _,
@@ -234,7 +236,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
         rewrite [sub_self, abs_zero],
         apply add_invs_nonneg,
        intro Hnlt,
-       rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt), 
+       rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt),
                 (s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_lt Hnlt))],
        rewrite [(div_sub_div Hsp Hspn), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
        apply rat.le.trans,
@@ -327,7 +329,7 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
     existsi max (ps Hs Hsep) j,
     intro n Hn,
     have Hnz : s_inv Hs ((K₂ s (s_inv Hs)) * 2 * n) ≠ 0, from s_inv_ne_zero Hs Hsep _,
-    xrewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz), 
+    xrewrite [↑smul, ↑one, rat.mul.comm, -(mul_one_div_cancel Hnz),
             -rat.mul_sub_left_distrib, abs_mul],
     apply rat.le.trans,
     apply rat.mul_le_mul_of_nonneg_right,
@@ -343,8 +345,8 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
       apply pnat.mul_le_mul_left
     end,
     have Hnz' : s (((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n)) ≠ 0, from
-      s_ne_zero_of_ge_p Hs Hsep 
-        (show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n), 
+      s_ne_zero_of_ge_p Hs Hsep
+        (show ps Hs Hsep ≤ ((ps Hs Hsep) * (ps Hs Hsep)) * ((K₂ s (s_inv Hs)) * 2 * n),
           by rewrite *pnat_mul_assoc; apply pnat.mul_le_mul_right),
     xrewrite [(s_inv_of_sep_gt_p Hs Hsep Hp), (div_div Hnz')],
     apply rat.le.trans,
@@ -352,7 +354,7 @@ theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) : smul s (s_inv H
     apply Hs,
     apply le_of_lt,
     apply rat_of_pnat_is_pos,
-    xrewrite [rat.mul.left_distrib, pnat_mul_comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat_mul_assoc, 
+    xrewrite [rat.mul.left_distrib, pnat_mul_comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat_mul_assoc,
             *(@pnat_div_helper (K₂ s (s_inv Hs))), -*rat.mul.assoc, *pnat.inv_cancel,
             *one_mul, -(padd_halves j)],
     apply rat.add_le_add,
@@ -464,13 +466,13 @@ theorem inv_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s
        apply one_is_reg
      end)
   else
-    (have H : s_inv Hs = zero, from funext (λ n, dif_neg Hsep), 
-     have Hsept : ¬ sep t zero, from 
+    (have H : s_inv Hs = zero, from funext (λ n, dif_neg Hsep),
+     have Hsept : ¬ sep t zero, from
        assume H', Hsep (sep_of_equiv_sep Ht Hs (equiv.symm _ _ Heq) H'),
      have H' : s_inv Ht = zero, from funext (λ n, dif_neg Hsept),
      H'⁻¹ ▸ (H⁻¹ ▸ equiv.refl zero))
 
-theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s := 
+theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s :=
   begin
     rewrite [↑equiv, ↑sneg],
     intro n,
@@ -479,7 +481,7 @@ theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s :=
   end
 
 theorem s_neg_sub {s t : seq} (Hs : regular s) (Ht : regular t) :
-        sneg (sadd s (sneg t)) ≡ sadd t (sneg s) := 
+        sneg (sadd s (sneg t)) ≡ sadd t (sneg s) :=
   begin
     apply equiv.trans,
     rotate 3,
@@ -526,7 +528,7 @@ theorem s_le_total {s t : seq} (Hs : regular s) (Ht : regular t) : s_le s t ∨
       repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
     end
 
-theorem s_le_of_not_lt {s t : seq} (Hle : ¬ s_lt s t) : s_le t s := 
+theorem s_le_of_not_lt {s t : seq} (Hle : ¬ s_lt s t) : s_le t s :=
   begin
     rewrite [↑s_le, ↑nonneg, ↑s_lt at Hle, ↑pos at Hle],
     let Hle' := forall_of_not_exists Hle,
@@ -552,11 +554,11 @@ theorem s_zero_inv_equiv_zero : s_inv zero_is_reg ≡ zero :=
   by rewrite s_inv_zero; apply equiv.refl
 
 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 := 
+        s_lt s t ∨ s ≡ t :=
   if H : s ≡ t then or.inr H else
     or.inl (lt_of_le_and_sep Hs Ht (and.intro Hle (sep_of_nequiv Hs Ht H)))
 
-theorem s_le_of_equiv_le_left {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) 
+theorem s_le_of_equiv_le_left {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
         (Heq : s ≡ t) (Hle : s_le s u) : s_le t u :=
   begin
     rewrite ↑s_le at *,
@@ -570,7 +572,7 @@ theorem s_le_of_equiv_le_left {s t u : seq} (Hs : regular s) (Ht : regular t) (H
     repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
   end
 
-theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) 
+theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
         (Heq : t ≡ u) (Hle : s_le s t) : s_le s u :=
   begin
     rewrite ↑s_le at *,
@@ -585,13 +587,13 @@ theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (
 
 -----------------------------
 
-definition r_inv (s : reg_seq) : reg_seq := reg_seq.mk (s_inv (reg_seq.is_reg s))  
-  (if H : sep (reg_seq.sq s) zero then reg_inv_reg (reg_seq.is_reg s) H else 
+definition r_inv (s : reg_seq) : reg_seq := reg_seq.mk (s_inv (reg_seq.is_reg s))
+  (if H : sep (reg_seq.sq s) zero then reg_inv_reg (reg_seq.is_reg s) H else
     have Hz : s_inv (reg_seq.is_reg s) = zero, from funext (λ n, dif_neg H), Hz⁻¹ ▸ zero_is_reg)
 
-theorem r_inv_zero : requiv (r_inv r_zero) r_zero := 
+theorem r_inv_zero : requiv (r_inv r_zero) r_zero :=
   s_zero_inv_equiv_zero
-  
+
 
 theorem r_inv_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_inv s) (r_inv t) :=
   inv_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) H
@@ -599,7 +601,7 @@ theorem r_inv_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_inv s) (
 theorem r_le_total (s t : reg_seq) : r_le s t ∨ r_le t s :=
   s_le_total (reg_seq.is_reg s) (reg_seq.is_reg t)
 
-theorem r_mul_inv (s : reg_seq) (Hsep : r_sep s r_zero) : requiv (s * (r_inv s)) r_one := 
+theorem r_mul_inv (s : reg_seq) (Hsep : r_sep s r_zero) : requiv (s * (r_inv s)) r_one :=
   mul_inv (reg_seq.is_reg s) Hsep
 
 theorem r_sep_of_nequiv (s t : reg_seq) (Hneq : ¬ requiv s t) : r_sep s t :=
@@ -626,7 +628,7 @@ postfix `⁻¹` := inv
 theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x :=
   quot.induction_on₂ x y (λ s t, s.r_le_total s t)
 
-theorem mul_inv' (x : ℝ) : x ≢ zero → x * x⁻¹ = one := 
+theorem mul_inv' (x : ℝ) : x ≢ zero → x * x⁻¹ = one :=
   quot.induction_on x (λ s H, quot.sound (s.r_mul_inv s H))
 
 theorem inv_mul' (x : ℝ) : x ≢ zero → x⁻¹ * x = one :=
@@ -639,7 +641,7 @@ theorem sep_of_neq {x y : ℝ} : ¬ x = y → x ≢ y :=
   quot.induction_on₂ x y (λ s t H, s.r_sep_of_nequiv s t (assume Heq, H (quot.sound Heq)))
 
 theorem sep_is_neq (x y : ℝ) : (x ≢ y) = (¬ x = y) :=
-  propext (iff.intro neq_of_sep sep_of_neq) 
+  propext (iff.intro neq_of_sep sep_of_neq)
 
 theorem mul_inv (x : ℝ) : x ≠ zero → x * x⁻¹ = one := !sep_is_neq ▸ !mul_inv'
 
@@ -648,15 +650,15 @@ theorem inv_mul (x : ℝ) : x ≠ zero → x⁻¹ * x = one := !sep_is_neq ▸ !
 theorem inv_zero : zero⁻¹ = zero := quot.sound (s.r_inv_zero)
 
 theorem lt_or_eq_of_le (x y : ℝ) : x ≤ y → x < y ∨ x = y :=
-  quot.induction_on₂ x y (λ s t H, or.elim (s.r_lt_or_equiv_of_le s t H) 
+  quot.induction_on₂ x y (λ s t H, or.elim (s.r_lt_or_equiv_of_le s t H)
     (assume H1, or.inl H1)
     (assume H2, or.inr (quot.sound H2)))
 
-theorem le_iff_lt_or_eq (x y : ℝ) : x ≤ y ↔ x < y ∨ x = y := 
+theorem le_iff_lt_or_eq (x y : ℝ) : x ≤ y ↔ x < y ∨ x = y :=
   iff.intro (lt_or_eq_of_le x y) (le_of_lt_or_eq x y)
 
-theorem dec_lt : decidable_rel lt := 
-  begin 
+theorem dec_lt : decidable_rel lt :=
+  begin
     rewrite ↑decidable_rel,
     intros,
     apply prop_decidable
@@ -664,7 +666,7 @@ theorem dec_lt : decidable_rel lt :=
 
 open [classes] algebra
 definition linear_ordered_field [instance] : algebra.discrete_linear_ordered_field ℝ :=
-  ⦃ algebra.discrete_linear_ordered_field, comm_ring, ordered_ring, 
+  ⦃ algebra.discrete_linear_ordered_field, comm_ring, ordered_ring,
     le_total := le_total,
     mul_inv_cancel := mul_inv,
     inv_mul_cancel := inv_mul,
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index b00093f842..109e6392fa 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -12,10 +12,12 @@ To do:
 -/
 
 import data.real.basic data.rat data.nat
-open -[coercions] rat 
+open -[coercions] rat
 open -[coercions] nat
 open eq eq.ops
- 
+local notation 0 := rat.of_num 0
+local notation 1 := rat.of_num 1
+
 ----------------------------------------------------------------------------------------------------
 
 -- pnat theorems
@@ -28,7 +30,7 @@ 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 := 
+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
@@ -40,12 +42,12 @@ theorem rewrite_helper8 (a b c : ℚ) : a - b = c - b + (a - c) := sorry -- simp
 
 ---------
 namespace s
-definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n) 
+definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
 
 definition nonneg (s : seq) := ∀ n : ℕ+, -(n⁻¹) ≤ s n
 
 theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
-        ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹ := 
+        ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹ :=
   begin
     apply exists.elim H,
     intro n Hn,
@@ -73,7 +75,7 @@ theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
     apply Hin
   end
 
-theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹) : pos s := 
+theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (s n) ≥ N⁻¹) : pos s :=
   begin
     rewrite ↑pos,
     apply exists.elim H,
@@ -87,11 +89,11 @@ theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (
   end
 
 theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) :
-        ∀ n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹ := 
+        ∀ n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹ :=
   begin
     intros,
     existsi n,
-    intro m Hm, 
+    intro m Hm,
     rewrite ↑nonneg at H,
     apply le.trans,
     apply neg_le_neg,
@@ -100,8 +102,8 @@ theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) :
     apply H
   end
 
-theorem nonneg_of_bdd_within {s : seq} (Hs : regular s) 
-        (H : ∀n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹) : nonneg s := 
+theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
+        (H : ∀n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹) : nonneg s :=
   begin
     rewrite ↑nonneg,
     intro k,
@@ -272,7 +274,7 @@ theorem s_neg_add_eq_s_add_neg (s t : seq) : sneg (sadd s t) ≡ sadd (sneg s) (
     apply add_invs_nonneg
   end
 
-theorem equiv_cancel_middle {s t u : seq} (Hs : regular s) (Ht : regular t) 
+theorem equiv_cancel_middle {s t u : seq} (Hs : regular s) (Ht : regular t)
         (Hu : regular u) : sadd (sadd u t) (sneg (sadd u s)) ≡ sadd t (sneg s) :=
   begin
     let Hz := zero_is_reg,
@@ -315,15 +317,15 @@ theorem add_le_add_of_le_right {s t : seq} (Hs : regular s) (Ht : regular t) (Ls
   begin
     intro u Hu,
     rewrite [↑s_le at *],
-    apply nonneg_of_nonneg_equiv, 
+    apply nonneg_of_nonneg_equiv,
     rotate 2,
     apply equiv.symm,
     apply equiv_cancel_middle,
     repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
   end
 
-theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s_lt s t) {u : seq} 
-        (Hu : regular u) : s_lt (sadd u s) (sadd u t) := 
+theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s_lt s t) {u : seq}
+        (Hu : regular u) : s_lt (sadd u s) (sadd u t) :=
   begin
     rewrite ↑s_lt at *,
     apply pos_of_pos_equiv,
@@ -333,7 +335,7 @@ theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s
     repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
   end
 
-theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonneg (sadd s t) := 
+theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) : nonneg (sadd s t) :=
   begin
     rewrite [↑nonneg at *, ↑sadd],
     intros,
@@ -351,7 +353,7 @@ theorem le.trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u
     have H' : nonneg (sadd (sadd u (sadd (sneg t) t)) (sneg s)), begin
       apply nonneg_of_nonneg_equiv,
       rotate 2,
-      apply add_well_defined, 
+      apply add_well_defined,
       rotate 4,
       apply s_add_assoc,
       repeat (apply reg_add_reg | apply reg_neg_reg | assumption),
@@ -427,7 +429,7 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
       sadd t (sneg s) n ≥ sadd t (sneg s) N -  N⁻¹ - n⁻¹ : Habs
       ... ≥ 0 - n⁻¹: begin
                        apply rat.sub_le_sub_right,
-                       apply le_of_lt, 
+                       apply le_of_lt,
                        apply (iff.mp' (sub_pos_iff_lt _ _)),
                        apply HN
                      end
@@ -462,11 +464,11 @@ theorem s_neg_zero : sneg zero ≡ zero :=
   begin
     rewrite ↑[sneg, zero, equiv],
     intros,
-    rewrite [sub_zero, abs_neg, abs_zero], 
+    rewrite [sub_zero, abs_neg, abs_zero],
     apply add_invs_nonneg
   end
 
-theorem s_sub_zero {s : seq} (Hs : regular s) : sadd s (sneg zero) ≡ s := 
+theorem s_sub_zero {s : seq} (Hs : regular s) : sadd s (sneg zero) ≡ s :=
   begin
     apply equiv.trans,
     rotate 3,
@@ -488,7 +490,7 @@ theorem s_pos_of_gt_zero {s : seq} (Hs : regular s) (Hgz : s_lt zero s) : pos s
     apply zero_is_reg
   end
 
-theorem s_gt_zero_of_pos {s : seq} (Hs : regular s) (Hp : pos s) : s_lt zero s := 
+theorem s_gt_zero_of_pos {s : seq} (Hs : regular s) (Hp : pos s) : s_lt zero s :=
   begin
     rewrite ↑s_lt,
     apply pos_of_pos_equiv,
@@ -498,7 +500,7 @@ theorem s_gt_zero_of_pos {s : seq} (Hs : regular s) (Hp : pos s) : s_lt zero s :
     repeat assumption
   end
 
-theorem s_nonneg_of_ge_zero {s : seq} (Hs : regular s) (Hgz : s_le zero s) : nonneg s := 
+theorem s_nonneg_of_ge_zero {s : seq} (Hs : regular s) (Hgz : s_le zero s) : nonneg s :=
   begin
     rewrite ↑s_le at *,
     apply nonneg_of_nonneg_equiv,
@@ -507,7 +509,7 @@ theorem s_nonneg_of_ge_zero {s : seq} (Hs : regular s) (Hgz : s_le zero s) : non
     repeat (assumption | apply reg_add_reg | apply reg_neg_reg | apply zero_is_reg)
   end
 
-theorem s_ge_zero_of_nonneg {s : seq} (Hs : regular s) (Hn : nonneg s) : s_le zero s := 
+theorem s_ge_zero_of_nonneg {s : seq} (Hs : regular s) (Hn : nonneg s) : s_le zero s :=
   begin
     rewrite ↑s_le,
     apply nonneg_of_nonneg_equiv,
@@ -567,7 +569,7 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
 
 theorem s_mul_gt_zero_of_gt_zero {s t : seq} (Hs : regular s) (Ht : regular t)
         (Hzs : s_lt zero s) (Hzt : s_lt zero t) : s_lt zero (smul s t) :=
-  s_gt_zero_of_pos 
+  s_gt_zero_of_pos
     (reg_mul_reg Hs Ht)
     (s_mul_pos_of_pos Hs Ht (s_pos_of_gt_zero Hs Hzs) (s_pos_of_gt_zero Ht Hzt))
 
@@ -619,7 +621,7 @@ theorem s_mul_nonneg_of_pos_of_zero {s t : seq} (Hs : regular s) (Ht : regular t
     repeat (assumption | apply reg_mul_reg | apply zero_is_reg)
   end
 
-theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t) 
+theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
         (Hps : nonneg s) (Hpt : nonneg t) : nonneg (smul s t) :=
   begin
     intro n,
@@ -784,7 +786,7 @@ theorem lt_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu :
 
 
 theorem sep_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
-        (Hv : regular v) (Hsu : s ≡ u) (Htv : t ≡ v) : s ≢ t ↔ u ≢ v := 
+        (Hv : regular v) (Hsu : s ≡ u) (Htv : t ≡ v) : s ≢ t ↔ u ≢ v :=
   begin
     rewrite ↑sep,
     apply iff.intro,
@@ -819,7 +821,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
       intro m,
       rewrite [↑sadd, ↑sneg, -rewrite_helper8]
-    end, 
+    end,
     rewrite [↑s_lt at *, ↑s_le at *],
     apply exists.elim (bdd_away_of_pos Rtns Hst),
     intro Nt HNt,
@@ -859,7 +861,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
       intro m,
       rewrite [↑sadd, ↑sneg, -rewrite_helper8]
-    end, 
+    end,
     rewrite [↑s_lt at *, ↑s_le at *],
     apply exists.elim (bdd_away_of_pos Runt Htu),
     intro Nu HNu,
@@ -938,7 +940,7 @@ theorem r_le.refl (s : reg_seq) : r_le s s := le.refl (reg_seq.is_reg s)
 theorem r_le.trans {s t u : reg_seq} (Hst : r_le s t) (Htu : r_le t u) : r_le s u :=
   le.trans (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u) Hst Htu
 
-theorem r_equiv_of_le_of_ge {s t : reg_seq} (Hs : r_le s t) (Hu : r_le t s) : 
+theorem r_equiv_of_le_of_ge {s t : reg_seq} (Hs : r_le s t) (Hu : r_le t s) :
         requiv s t :=
   equiv_of_le_of_ge (reg_seq.is_reg s) (reg_seq.is_reg t) Hs Hu
 
@@ -950,14 +952,14 @@ theorem r_add_le_add_of_le_right {s t : reg_seq} (H : r_le s t) (u : reg_seq) :
   add_le_add_of_le_right (reg_seq.is_reg s) (reg_seq.is_reg t) H
                                         (reg_seq.sq u) (reg_seq.is_reg u)
 
-theorem r_add_le_add_of_le_right_var (s t u : reg_seq) (H : r_le s t) : 
+theorem r_add_le_add_of_le_right_var (s t u : reg_seq) (H : r_le s t) :
         r_le (u + s) (u + t) := r_add_le_add_of_le_right H u
 
-theorem r_mul_pos_of_pos {s t : reg_seq} (Hs : r_lt r_zero s) (Ht : r_lt r_zero t) : 
+theorem r_mul_pos_of_pos {s t : reg_seq} (Hs : r_lt r_zero s) (Ht : r_lt r_zero t) :
         r_lt r_zero (s * t) :=
   s_mul_gt_zero_of_gt_zero (reg_seq.is_reg s) (reg_seq.is_reg t) Hs Ht
 
-theorem r_mul_nonneg_of_nonneg {s t : reg_seq} (Hs : r_le r_zero s) (Ht : r_le r_zero t) : 
+theorem r_mul_nonneg_of_nonneg {s t : reg_seq} (Hs : r_le r_zero s) (Ht : r_le r_zero t) :
         r_le r_zero (s * t) :=
   s_mul_ge_zero_of_ge_zero (reg_seq.is_reg s) (reg_seq.is_reg t) Hs Ht
 
@@ -1036,7 +1038,7 @@ theorem mul_ge_zero_of_ge_zero (x y : ℝ) : zero ≤ x → zero ≤ y → zero
 
 theorem not_sep_self (x : ℝ) : ¬ x ≢ x :=
   quot.induction_on x (λ s, s.r_not_sep_self s)
- 
+
 theorem not_lt_self (x : ℝ) : ¬ x < x :=
   quot.induction_on x (λ s, s.r_not_lt_self s)
 
@@ -1049,7 +1051,7 @@ theorem lt_of_le_of_lt (x y z : ℝ) : x ≤ y → y < z → x < z :=
 theorem lt_of_lt_of_le (x y z : ℝ) : x < y → y ≤ z → x < z :=
   quot.induction_on₃ x y z (λ s t u H H', s.r_lt_of_lt_of_le H H')
 
-theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y := 
+theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y :=
   quot.induction_on₃ x y z (λ s t u, s.r_add_lt_add_left_var s t u)
 
 theorem add_lt_add_left (x y : ℝ) : x < y → ∀ z : ℝ, z + x < z + y :=
@@ -1059,8 +1061,8 @@ theorem zero_lt_one : zero < one := s.r_zero_lt_one
 
 theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
     (quot.induction_on₂ x y (λ s t H, or.elim H (take H', begin
-        apply s.r_le_of_lt_or_eq, 
-        apply or.inl H' 
+        apply s.r_le_of_lt_or_eq,
+        apply or.inl H'
       end)
       (take H', begin
         apply s.r_le_of_lt_or_eq,
@@ -1071,11 +1073,11 @@ theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
 -- 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) 
+    (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), 
+        let H'' := iff.mp' (s.r_le_iff_lt_or_equiv s t),
         apply H'' (or.inl H')
       end)
       (take H', begin
@@ -1105,7 +1107,7 @@ definition ordered_ring  : algebra.ordered_ring ℝ :=
 
 -----------------------------------
 --- 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) := sorry
 
 /-theorem sep_is_eq (x y : ℝ) : x ≢ y = ¬ (x = y) := begin
    apply propext,