diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index b584aaa01..03edc762f 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -512,7 +512,7 @@ section migrate_algebra
     add_comm         := add.comm,
     mul              := mul,
     mul_assoc        := mul.assoc,
-    one              := (of_num 1),
+    one              := 1,
     one_mul          := one_mul,
     mul_one          := mul_one,
     left_distrib     := mul.left_distrib,
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index d161ee493..4f642e9f8 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -1029,10 +1029,17 @@ definition neg (x : ℝ) : ℝ :=
                                    quot.sound (rneg_well_defined Hab)))
 prefix [priority real.prio] `-` := neg
 
-definition zero : ℝ := quot.mk r_zero
+open rat -- no coercions before
+
+definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (s.r_const a)
+definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n)
+
+--definition zero : ℝ := 0
+--definition one : ℝ := 1
+--definition zero : ℝ := quot.mk r_zero
 --notation 0 := zero
 
-definition one : ℝ := quot.mk r_one
+--definition one : ℝ := quot.mk r_one
 
 theorem add_comm (x y : ℝ) : x + y = y + x :=
   quot.induction_on₂ x y (λ s t, quot.sound (r_add_comm s t))
@@ -1040,13 +1047,13 @@ theorem add_comm (x y : ℝ) : x + y = y + x :=
 theorem add_assoc (x y z : ℝ) : x + y + z = x + (y + z) :=
   quot.induction_on₃ x y z (λ s t u, quot.sound (r_add_assoc s t u))
 
-theorem zero_add (x : ℝ) : zero + x = x :=
+theorem zero_add (x : ℝ) : 0 + x = x :=
   quot.induction_on x (λ s, quot.sound (r_zero_add s))
 
-theorem add_zero (x : ℝ) : x + zero = x :=
+theorem add_zero (x : ℝ) : x + 0 = x :=
   quot.induction_on x (λ s, quot.sound (r_add_zero s))
 
-theorem neg_cancel (x : ℝ) : -x + x = zero :=
+theorem neg_cancel (x : ℝ) : -x + x = 0 :=
   quot.induction_on x (λ s, quot.sound (r_neg_cancel s))
 
 theorem mul_assoc (x y z : ℝ) : x * y * z = x * (y * z) :=
@@ -1055,10 +1062,10 @@ theorem mul_assoc (x y z : ℝ) : x * y * z = x * (y * z) :=
 theorem mul_comm (x y : ℝ) : x * y = y * x :=
   quot.induction_on₂ x y (λ s t, quot.sound (r_mul_comm s t))
 
-theorem one_mul (x : ℝ) : one * x = x :=
+theorem one_mul (x : ℝ) : 1 * x = x :=
   quot.induction_on x (λ s, quot.sound (r_one_mul s))
 
-theorem mul_one (x : ℝ) : x * one = x :=
+theorem mul_one (x : ℝ) : x * 1 = x :=
   quot.induction_on x (λ s, quot.sound (r_mul_one s))
 
 theorem distrib (x y z : ℝ) : x * (y + z) = x * y + x * z :=
@@ -1067,8 +1074,8 @@ 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 :=
-  take H : zero = one,
+theorem zero_ne_one : ¬ (0 : ℝ) = 1 :=
+  take H : 0 = 1,
   absurd (quot.exact H) (r_zero_nequiv_one)
 
 protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
@@ -1076,7 +1083,7 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
     fapply algebra.comm_ring.mk,
     exact add,
     exact add_assoc,
-    exact zero,
+    exact of_num 0,
     exact zero_add,
     exact add_zero,
     exact neg,
@@ -1084,7 +1091,7 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
     exact add_comm,
     exact mul,
     exact mul_assoc,
-    apply one,
+    apply of_num 1,
     apply one_mul,
     apply mul_one,
     apply distrib,
@@ -1092,10 +1099,6 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
     apply mul_comm
   end
 
-open rat -- no coercions before
-
-definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (s.r_const a)
-
 theorem of_rat_add (a b : ℚ) : of_rat a + of_rat b = of_rat (a + b) :=
    quot.sound (s.r_add_consts a b)
 
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index b91cdfb36..734dc7adc 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -584,10 +584,10 @@ postfix [priority real.prio] `⁻¹` := 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 ≢ 0 → x * x⁻¹ = 1 :=
   quot.induction_on x (λ s H, quot.sound (s.r_mul_inv s H))
 
-theorem inv_mul' (x : ℝ) : x ≢ zero → x⁻¹ * x = one :=
+theorem inv_mul' (x : ℝ) : x ≢ 0 → x⁻¹ * x = 1 :=
   by rewrite real.mul_comm; apply mul_inv'
 
 theorem neq_of_sep {x y : ℝ} (H : x ≢ y) : ¬ x = y :=
@@ -599,11 +599,11 @@ theorem sep_of_neq {x y : ℝ} : ¬ x = y → x ≢ y :=
 theorem sep_is_neq (x y : ℝ) : (x ≢ y) = (¬ x = y) :=
   propext (iff.intro neq_of_sep sep_of_neq)
 
-theorem mul_inv (x : ℝ) : x ≠ zero → x * x⁻¹ = one := !sep_is_neq ▸ !mul_inv'
+theorem mul_inv (x : ℝ) : x ≠ 0 → x * x⁻¹ = 1 := !sep_is_neq ▸ !mul_inv'
 
-theorem inv_mul (x : ℝ) : x ≠ zero → x⁻¹ * x = one := !sep_is_neq ▸ !inv_mul'
+theorem inv_mul (x : ℝ) : x ≠ 0 → x⁻¹ * x = 1 := !sep_is_neq ▸ !inv_mul'
 
-theorem inv_zero : zero⁻¹ = zero := quot.sound (s.r_inv_zero)
+theorem inv_zero : (0 : ℝ)⁻¹ = 0 := 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)
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 7dbddd440..bb8b22982 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -17,8 +17,6 @@ local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
 local notation 2 := subtype.tag (of_num 2) dec_trivial
 
-----------------------------------------------------------------------------------------------------
-
 namespace s
 definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
 
@@ -1026,8 +1024,8 @@ definition lt (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_lt a b) s.r_lt_wel
 infix [priority real.prio] `<` := lt
 
 definition le (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_le a b) s.r_le_well_defined
-infix [priority real.prio] `≤` := le
 infix [priority real.prio] `<=` := le
+infix [priority real.prio] `≤` := le
 
 definition gt [reducible] (a b : ℝ) := lt b a
 definition ge [reducible] (a b : ℝ) := le b a
@@ -1084,7 +1082,7 @@ theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y :=
 theorem add_lt_add_left (x y : ℝ) : x < y → ∀ z : ℝ, z + x < z + y :=
   take H z, add_lt_add_left_var x y z H
 
-theorem zero_lt_one : zero < one := s.r_zero_lt_one
+theorem zero_lt_one : (0 : ℝ) < (1 : ℝ) := 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