diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index c3754d372..c51933e0a 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -541,8 +541,6 @@ section migrate_algebra
   definition divide (a b : rat) := algebra.divide a b
   infix [priority rat.prio] `/` := divide
 
-  definition dvd (a b : rat) := algebra.dvd a b
-
   definition pow (a : ℚ) (n : ℕ) : ℚ := algebra.pow a n
   infix [priority rat.prio] ^ := pow
   definition nmul (n : ℕ) (a : ℚ) : ℚ := algebra.nmul n a
@@ -550,7 +548,11 @@ section migrate_algebra
   definition imul (i : ℤ) (a : ℚ) : ℚ := algebra.imul i a
 
   migrate from algebra with rat
-    replacing sub → rat.sub, divide → divide, dvd → dvd, pow → pow, nmul → nmul, imul → imul
+    hiding dvd, dvd.elim, dvd.elim_left, dvd.intro, dvd.intro_left, dvd.refl, dvd.trans,
+      dvd_mul_left, dvd_mul_of_dvd_left, dvd_mul_of_dvd_right, dvd_mul_right, dvd_neg_iff_dvd,
+      dvd_neg_of_dvd, dvd_of_dvd_neg, dvd_of_mul_left_dvd, dvd_of_mul_left_eq,
+      dvd_of_mul_right_dvd, dvd_of_mul_right_eq, dvd_of_neg_dvd, dvd_sub, dvd_zero
+    replacing sub → rat.sub, divide → divide, pow → pow, nmul → nmul, imul → imul
 
 end migrate_algebra
 
@@ -558,7 +560,7 @@ 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.mpr (!eq_div_iff_mul_eq H) (mul_denom a)
 
-theorem of_int_div {a b : ℤ} (H : b ∣ a) : of_int (a div b) = of_int a / of_int b :=
+theorem of_int_div {a b : ℤ} (H : (#int 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])
@@ -570,6 +572,10 @@ decidable.by_cases
           by rewrite [Hc, !int.mul_div_cancel_left bnz, mul.comm]),
     iff.mpr (!eq_div_iff_mul_eq bnz') H')
 
+theorem of_nat_div {a b : ℕ} (H : (#nat b ∣ a)) : of_nat (#nat a div b) = of_nat a / of_nat b :=
+have H' : (#int int.of_nat b ∣ int.of_nat a), by rewrite [int.of_nat_dvd_of_nat_iff]; exact H,
+by+ rewrite [of_nat_eq, int.of_nat_div, of_int_div H']
+
 theorem of_int_pow (a : ℤ) (n : ℕ) : of_int (a^n) = (of_int a)^n :=
 begin
   induction n with n ih,
@@ -577,4 +583,7 @@ begin
   rewrite [pow_succ, int.pow_succ, of_int_mul, ih]
 end
 
+theorem of_nat_pow (a : ℕ) (n : ℕ) : of_nat (#nat a^n) = (of_nat a)^n :=
+by rewrite [of_nat_eq, int.of_nat_pow, of_int_pow]
+
 end rat
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 14605aa4f..2f22b7ca6 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -331,7 +331,11 @@ section migrate_algebra
   definition sign : ℚ → ℚ := algebra.sign
 
   migrate from algebra with rat
-    replacing sub → sub, dvd → dvd, has_le.ge → ge, has_lt.gt → gt,
+    hiding dvd, dvd.elim, dvd.elim_left, dvd.intro, dvd.intro_left, dvd.refl, dvd.trans,
+      dvd_mul_left, dvd_mul_of_dvd_left, dvd_mul_of_dvd_right, dvd_mul_right, dvd_neg_iff_dvd,
+      dvd_neg_of_dvd, dvd_of_dvd_neg, dvd_of_mul_left_dvd, dvd_of_mul_left_eq,
+      dvd_of_mul_right_dvd, dvd_of_mul_right_eq, dvd_of_neg_dvd, dvd_sub, dvd_zero
+    replacing sub → sub, has_le.ge → ge, has_lt.gt → gt,
               divide → divide, max → max, min → min, abs → abs, sign → sign,
               nmul → nmul, imul → imul
 
@@ -342,12 +346,41 @@ section migrate_algebra
 
 end migrate_algebra
 
-theorem rat_of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=
+theorem of_nat_abs (a : ℤ) : abs (of_int a) = of_nat (int.nat_abs a) :=
 assert ∀ n : ℕ, of_int (int.neg_succ_of_nat n) = - of_nat (nat.succ n), from λ n, rfl,
 int.induction_on a
   (take b, abs_of_nonneg !of_nat_nonneg)
   (take b, by rewrite [this, abs_neg, abs_of_nonneg !of_nat_nonneg])
 
+theorem eq_zero_of_nonneg_of_forall_lt {x : ℚ} (xnonneg : x ≥ 0) (H : ∀ ε, ε > 0 → x < ε) :
+  x = 0 :=
+  decidable.by_contradiction
+    (suppose x ≠ 0,
+      have x > 0, from lt_of_le_of_ne xnonneg (ne.symm this),
+      have x < x, from H x this,
+      show false, from !lt.irrefl this)
+
+theorem eq_zero_of_nonneg_of_forall_le {x : ℚ} (xnonneg : x ≥ 0) (H : ∀ ε, ε > 0 → x ≤ ε) :
+  x = 0 :=
+have H' : ∀ ε, ε > 0 → x < ε, from
+  take ε, suppose ε > 0,
+  have ε / 2 > 0, from div_pos_of_pos_of_pos this two_pos,
+  have x ≤ ε / 2, from H _ this,
+  show x < ε, from lt_of_le_of_lt this (rat.div_two_lt_of_pos `ε > 0`),
+eq_zero_of_nonneg_of_forall_lt xnonneg H'
+
+theorem eq_zero_of_forall_abs_le {x : ℚ} (H : ∀ ε, ε > 0 → abs x ≤ ε) :
+  x = 0 :=
+decidable.by_contradiction
+  (suppose x ≠ 0,
+    have abs x = 0, from eq_zero_of_nonneg_of_forall_le !abs_nonneg H,
+    show false, from `x ≠ 0` (eq_zero_of_abs_eq_zero this))
+
+theorem eq_of_forall_abs_sub_le {x y : ℚ} (H : ∀ ε, ε > 0 → abs (x - y) ≤ ε) :
+  x = y :=
+have x - y = 0, from eq_zero_of_forall_abs_le H,
+eq_of_sub_eq_zero this
+
 section
   open int
 
@@ -411,7 +444,7 @@ calc
     a ≤ abs a                                   : le_abs_self
   ... ≤ abs (of_int (num a))                    : this
   ... ≤ abs (of_int (num a)) + 1                : rat.le_add_of_nonneg_right trivial
-  ... = of_nat (int.nat_abs (num a)) + 1        : rat_of_nat_abs
+  ... = of_nat (int.nat_abs (num a)) + 1        : of_nat_abs
   ... = of_nat (nat.succ (int.nat_abs (num a))) : of_nat_add
 
 theorem ubound_pos (a : ℚ) : nat.gt (ubound a) nat.zero := !nat.succ_pos
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 67e023000..de666d3c9 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -904,6 +904,22 @@ theorem mul_consts (a b : ℚ) : smul (const a) (const b) ≡ const (a * b) :=
 theorem neg_const (a : ℚ) : sneg (const a) ≡ const (-a) :=
   by apply equiv.refl
 
+section
+  open rat
+
+  lemma eq_of_const_equiv {a b : ℚ} (H : const a ≡ const b) : a = b :=
+  have H₁ : ∀ n : ℕ+, abs (a - b) ≤ n⁻¹ + n⁻¹, from H,
+  eq_of_forall_abs_sub_le
+    (take ε,
+      suppose ε > 0,
+      have ε / 2 > 0, from div_pos_of_pos_of_pos this two_pos,
+      obtain n (Hn : n⁻¹ ≤ ε / 2), from pnat_bound this,
+      show abs (a - b) ≤ ε, from calc
+        abs (a - b) ≤ n⁻¹ + n⁻¹     : H₁ n
+                ... ≤ ε / 2 + ε / 2 : add_le_add Hn Hn
+                ... = ε             : rat.add_halves)
+end
+
 ---------------------------------------------
 -- create the type of regular sequences and lift theorems
 
@@ -1025,15 +1041,10 @@ prefix [priority real.prio] `-` := neg
 open rat -- no coercions before
 
 definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (r_const a)
+definition of_int [coercion] (i : ℤ) : ℝ := int.to.real i
+definition of_nat [coercion] (n : ℕ) : ℝ := nat.to.real n
 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
-
 theorem add_comm (x y : ℝ) : x + y = y + x :=
   quot.induction_on₂ x y (λ s t, quot.sound (r_add_comm s t))
 
@@ -1092,15 +1103,62 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
     apply mul_comm
   end
 
-theorem of_rat_add (a b : ℚ) : of_rat a + of_rat b = of_rat (a + b) :=
+theorem of_int_eq (a : ℤ) : of_int a = of_rat (rat.of_int a) := rfl
+
+theorem of_nat_eq (a : ℕ) : of_nat a = of_rat (rat.of_nat a) := rfl
+
+theorem of_rat.inj {x y : ℚ} (H : of_rat x = of_rat y) : x = y :=
+eq_of_const_equiv (quot.exact H)
+
+theorem eq_of_of_rat_eq_of_rat {x y : ℚ} (H : of_rat x = of_rat y) : x = y :=
+of_rat.inj H
+
+theorem of_rat_eq_of_rat_iff (x y : ℚ) : of_rat x = of_rat y ↔ x = y :=
+iff.intro eq_of_of_rat_eq_of_rat !congr_arg
+
+theorem of_int.inj {a b : ℤ} (H : of_int a = of_int b) : a = b :=
+rat.of_int.inj (of_rat.inj H)
+
+theorem eq_of_of_int_eq_of_int {a b : ℤ} (H : of_int a = of_int b) : a = b :=
+of_int.inj H
+
+theorem of_int_eq_of_int_iff (a b : ℤ) : of_int a = of_int b ↔ a = b :=
+iff.intro of_int.inj !congr_arg
+
+theorem of_nat.inj {a b : ℕ} (H : of_nat a = of_nat b) : a = b :=
+int.of_nat.inj (of_int.inj H)
+
+theorem eq_of_of_nat_eq_of_nat {a b : ℕ} (H : of_nat a = of_nat b) : a = b :=
+of_nat.inj H
+
+theorem of_nat_eq_of_nat_iff (a b : ℕ) : of_nat a = of_nat b ↔ a = b :=
+iff.intro of_nat.inj !congr_arg
+
+theorem of_rat_add (a b : ℚ) : of_rat (a + b) = of_rat a + of_rat b :=
    quot.sound (r_add_consts a b)
 
-theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a := eq.symm (quot.sound (r_neg_const a))
+theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a :=
+  eq.symm (quot.sound (r_neg_const a))
 
-theorem of_rat_mul (a b : ℚ) : of_rat a * of_rat b = of_rat (a * b) :=
+theorem of_rat_mul (a b : ℚ) : of_rat (a * b) = of_rat a * of_rat b :=
   quot.sound (r_mul_consts a b)
 
+theorem of_int_add (a b : ℤ) : of_int (#int a + b) = of_int a + of_int b :=
+  by rewrite [of_int_eq, rat.of_int_add, of_rat_add]
+
+theorem of_int_neg (a : ℤ) : of_int (#int -a) = -of_int a :=
+  by rewrite [of_int_eq, rat.of_int_neg, of_rat_neg]
+
+theorem of_int_mul (a b : ℤ) : of_int (#int a * b) = of_int a * of_int b :=
+  by rewrite [of_int_eq, rat.of_int_mul, of_rat_mul]
+
+theorem of_nat_add (a b : ℕ) : of_nat (#nat a + b) = of_nat a + of_nat b :=
+  by rewrite [of_nat_eq, rat.of_nat_add, of_rat_add]
+
+theorem of_nat_mul (a b : ℕ) : of_nat (#nat a * b) = of_nat a * of_nat b :=
+  by rewrite [of_nat_eq, rat.of_nat_mul, of_rat_mul]
+
 theorem add_half_of_rat (n : ℕ+) : of_rat (2 * n)⁻¹ + of_rat (2 * n)⁻¹ = of_rat (n⁻¹) :=
-  by rewrite [of_rat_add, pnat.add_halves]
+  by rewrite [-of_rat_add, pnat.add_halves]
 
 end real
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index 6b93a5db1..edfba26fc 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -232,7 +232,7 @@ theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : c
     krewrite abs_neg,
     apply Hc,
     apply Hn,
-    xrewrite of_rat_add,
+    xrewrite -of_rat_add,
     apply of_rat_le_of_rat_of_le,
     rewrite pnat.add_halves,
     apply rat.le.refl
@@ -270,7 +270,7 @@ private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
     apply pnat.le.trans,
     apply Hmn,
     apply Nb_spec_right,
-    rewrite [*of_rat_add, rat.add.assoc, pnat.add_halves],
+    rewrite [-*of_rat_add, rat.add.assoc, pnat.add_halves],
     apply of_rat_le_of_rat_of_le,
     apply rat.add_le_add_right,
     apply inv_ge_of_le,
@@ -281,8 +281,8 @@ theorem lim_seq_reg : rat_seq.regular lim_seq :=
   begin
     rewrite ↑rat_seq.regular,
     intro m n,
-    apply le_of_rat_le_of_rat,
-    rewrite [abs_const, -of_rat_sub, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
+    apply le_of_of_rat_le_of_rat,
+    rewrite [abs_const, of_rat_sub, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
     apply real.le.trans,
     apply abs_add_three,
     cases em (M (2 * m) ≥ M (2 * n)) with [Hor1, Hor2],
@@ -345,7 +345,7 @@ theorem converges_of_cauchy : converges_to X lim (Nb M) :=
     rewrite ↑lim_seq,
     apply approx_spec,
     apply lim_spec,
-    rewrite 2 of_rat_add,
+    rewrite [-*of_rat_add],
     apply of_rat_le_of_rat_of_le,
     apply rat.le.trans,
     apply rat.add_le_add_three,
@@ -375,7 +375,7 @@ section ints
 
 open int
 
-theorem archimedean_upper (x : ℝ) : ∃ z : ℤ, x ≤ of_rat (of_int z) :=
+theorem archimedean_upper (x : ℝ) : ∃ z : ℤ, x ≤ of_int z :=
   begin
     apply quot.induction_on x,
     intro s,
@@ -392,36 +392,35 @@ theorem archimedean_upper (x : ℝ) : ∃ z : ℤ, x ≤ of_rat (of_int z) :=
     apply H
   end
 
-theorem archimedean_upper_strict (x : ℝ) : ∃ z : ℤ, x < of_rat (of_int z) :=
+theorem archimedean_upper_strict (x : ℝ) : ∃ z : ℤ, x < of_int z :=
   begin
     cases archimedean_upper x with [z, Hz],
     existsi z + 1,
     apply lt_of_le_of_lt,
     apply Hz,
-    apply of_rat_lt_of_rat_of_lt,
     apply of_int_lt_of_int_of_lt,
     apply int.lt_add_of_pos_right,
     apply dec_trivial
   end
 
-theorem archimedean_lower (x : ℝ) : ∃ z : ℤ, x ≥ of_rat (of_int z) :=
+theorem archimedean_lower (x : ℝ) : ∃ z : ℤ, x ≥ of_int z :=
   begin
     cases archimedean_upper (-x) with [z, Hz],
     existsi -z,
-    rewrite [of_int_neg, of_rat_neg],
+    rewrite [of_int_neg],
     apply iff.mp !neg_le_iff_neg_le Hz
   end
 
-theorem archimedean_lower_strict (x : ℝ) : ∃ z : ℤ, x > of_rat (of_int z) :=
+theorem archimedean_lower_strict (x : ℝ) : ∃ z : ℤ, x > of_int z :=
   begin
     cases archimedean_upper_strict (-x) with [z, Hz],
     existsi -z,
-    rewrite [of_int_neg, of_rat_neg],
+    rewrite [of_int_neg],
     apply iff.mp !neg_lt_iff_neg_lt Hz
   end
 
 definition ex_floor (x : ℝ) :=
-  (@ex_largest_of_bdd (λ z, x ≥ of_rat (of_int z)) _
+  (@ex_largest_of_bdd (λ z, x ≥ of_int z) _
     (begin
       existsi some (archimedean_upper_strict x),
       let Har := some_spec (archimedean_upper_strict x),
@@ -429,8 +428,7 @@ definition ex_floor (x : ℝ) :=
       apply not_le_of_gt,
       apply lt_of_lt_of_le,
       apply Har,
-      have H : of_rat (of_int (some (archimedean_upper_strict x))) ≤ of_rat (of_int z), begin
-        apply of_rat_le_of_rat_of_le,
+      have H : of_int (some (archimedean_upper_strict x)) ≤ of_int z, begin
         apply of_int_le_of_int_of_le,
         apply Hz
       end,
@@ -443,28 +441,28 @@ noncomputable definition floor (x : ℝ) : ℤ :=
 
 noncomputable definition ceil (x : ℝ) : ℤ := - floor (-x)
 
-theorem floor_spec (x : ℝ) : of_rat (of_int (floor x)) ≤ x :=
+theorem floor_spec (x : ℝ) : of_int (floor x) ≤ x :=
   and.left (some_spec (ex_floor x))
 
-theorem floor_largest {x : ℝ} {z : ℤ} (Hz : z > floor x) : x < of_rat (of_int z) :=
+theorem floor_largest {x : ℝ} {z : ℤ} (Hz : z > floor x) : x < of_int z :=
   begin
     apply lt_of_not_ge,
     cases some_spec (ex_floor x),
     apply a_1 _ Hz
   end
 
-theorem ceil_spec (x : ℝ) : of_rat (of_int (ceil x)) ≥ x :=
+theorem ceil_spec (x : ℝ) : of_int (ceil x) ≥ x :=
   begin
-    rewrite [↑ceil, of_int_neg, of_rat_neg],
+    rewrite [↑ceil, of_int_neg],
     apply iff.mp !le_neg_iff_le_neg,
     apply floor_spec
   end
 
-theorem ceil_smallest {x : ℝ} {z : ℤ} (Hz : z < ceil x) : x > of_rat (of_int z) :=
+theorem ceil_smallest {x : ℝ} {z : ℤ} (Hz : z < ceil x) : x > of_int z :=
   begin
     rewrite ↑ceil at Hz,
     let Hz' := floor_largest (iff.mp !int.lt_neg_iff_lt_neg Hz),
-    rewrite [of_int_neg at Hz', of_rat_neg at Hz'],
+    rewrite [of_int_neg at Hz'],
     apply lt_of_neg_lt_neg Hz'
   end
 
@@ -474,10 +472,10 @@ theorem floor_succ (x : ℝ) : (floor x) + 1 = floor (x + 1) :=
     intro H,
     cases int.lt_or_gt_of_ne H with [Hlt, Hgt],
     let Hl := floor_largest (iff.mp !int.add_lt_iff_lt_sub_right Hlt),
-    rewrite [of_int_sub at Hl, -of_rat_sub at Hl],
+    rewrite [of_int_sub at Hl],
     apply not_le_of_gt (iff.mpr !add_lt_iff_lt_sub_right Hl) !floor_spec,
     let Hl := floor_largest Hgt,
-    rewrite [of_int_add at Hl, -of_rat_add at Hl],
+    rewrite [of_int_add at Hl],
     apply not_le_of_gt (lt_of_add_lt_add_right Hl) !floor_spec
   end
 
@@ -548,11 +546,10 @@ noncomputable definition bisect (ab : ℚ × ℚ) :=
   else
     (avg (pr1 ab) (pr2 ab), pr2 ab)
 
-noncomputable definition under : ℚ := of_int (floor (elt - 1))
+noncomputable definition under : ℚ := rat.of_int (floor (elt - 1))
 
 theorem under_spec1 : of_rat under < elt :=
-  have H : of_rat under < of_rat (of_int (floor elt)), begin
-    apply of_rat_lt_of_rat_of_lt,
+  have H : of_rat under < of_int (floor elt), begin
     apply of_int_lt_of_int_of_lt,
     apply floor_succ_lt
   end,
@@ -569,11 +566,10 @@ theorem under_spec : ¬ ub under :=
     apply not_le_of_gt under_spec1
   end
 
-noncomputable definition over : ℚ := of_int (ceil (bound + 1)) -- b
+noncomputable definition over : ℚ := rat.of_int (ceil (bound + 1)) -- b
 
 theorem over_spec1 : bound < of_rat over :=
-  have H : of_rat (of_int (ceil bound)) < of_rat over, begin
-    apply of_rat_lt_of_rat_of_lt,
+  have H : of_int (ceil bound) < of_rat over, begin
     apply of_int_lt_of_int_of_lt,
     apply ceil_succ
   end,
@@ -651,11 +647,11 @@ theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / (rat.pow 2
               rat.sub_self_div_two]
     end)
 
-theorem binary_nat_bound (a : ℕ) : of_nat a ≤ (rat.pow 2 a) :=
+theorem binary_nat_bound (a : ℕ) : rat.of_nat a ≤ (rat.pow 2 a) :=
   nat.induction_on a (rat.zero_le_one)
    (take n, assume Hn,
     calc
-     of_nat (succ n) = (of_nat n) + 1 : of_nat_add
+     rat.of_nat (succ n) = (rat.of_nat n) + 1 : rat.of_nat_add
        ... ≤ rat.pow 2 n + 1 : rat.add_le_add_right Hn
        ... ≤ rat.pow 2 n + rat.pow 2 n :
              rat.add_le_add_left (rat.pow_ge_one_of_ge_one rat.two_ge_one _)
@@ -663,7 +659,7 @@ theorem binary_nat_bound (a : ℕ) : of_nat a ≤ (rat.pow 2 a) :=
 
 theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ rat.pow 2 n :=
   exists.intro (ubound a) (calc
-      a ≤ of_nat (ubound a) : ubound_ge
+      a ≤ rat.of_nat (ubound a) : ubound_ge
     ... ≤ rat.pow 2 (ubound a) : binary_nat_bound)
 
 theorem rat_power_two_le (k : ℕ+) : rat_of_pnat k ≤ rat.pow 2 k~ :=
@@ -739,7 +735,7 @@ theorem under_lt_over : under < over :=
   begin
     cases exists_not_of_not_forall under_spec with [x, Hx],
     cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu],
-    apply lt_of_rat_lt_of_rat,
+    apply lt_of_of_rat_lt_of_rat,
     apply lt_of_lt_of_le,
     apply lt_of_not_ge Hxu,
     apply over_spec _ HXx
@@ -750,7 +746,7 @@ theorem under_seq_lt_over_seq : ∀ m n : ℕ, under_seq m < over_seq n :=
     intros,
     cases exists_not_of_not_forall (PA m) with [x, Hx],
     cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu],
-    apply lt_of_rat_lt_of_rat,
+    apply lt_of_of_rat_lt_of_rat,
     apply lt_of_lt_of_le,
     apply lt_of_not_ge Hxu,
     apply PB,
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index 7e461c308..331d98c0a 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -653,10 +653,27 @@ section migrate_algebra
   noncomputable definition divide (a b : ℝ): ℝ := algebra.divide a b
 
   migrate from algebra with real
-    replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd,
+    hiding dvd, dvd.elim, dvd.elim_left, dvd.intro, dvd.intro_left, dvd.refl, dvd.trans,
+      dvd_mul_left, dvd_mul_of_dvd_left, dvd_mul_of_dvd_right, dvd_mul_right, dvd_neg_iff_dvd,
+      dvd_neg_of_dvd, dvd_of_dvd_neg, dvd_of_mul_left_dvd, dvd_of_mul_left_eq,
+      dvd_of_mul_right_dvd, dvd_of_mul_right_eq, dvd_of_neg_dvd, dvd_sub, dvd_zero
+    replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign,
       divide → divide, max → max, min → min, pow → pow, nmul → nmul, imul → imul
 end migrate_algebra
 
 infix / := divide
 
+theorem of_rat_divide (x y : ℚ) : of_rat (x / y) = of_rat x / of_rat y :=
+by_cases
+  (assume yz : y = 0, by rewrite [yz, rat.div_zero, real.div_zero])
+  (assume ynz : y ≠ 0,
+    have ynz' : of_rat y ≠ 0, from assume yz', ynz (of_rat.inj yz'),
+    !eq_div_of_mul_eq ynz' (by rewrite [-of_rat_mul, !rat.div_mul_cancel ynz]))
+
+theorem of_int_div (x y : ℤ) (H : (#int y ∣ x)) : of_int (#int x div y) = of_int x / of_int y :=
+by rewrite [of_int_eq, rat.of_int_div H, of_rat_divide]
+
+theorem of_nat_div (x y : ℕ) (H : (#nat y ∣ x)) : of_nat (#nat x div y) = of_nat x / of_nat y :=
+by rewrite [of_nat_eq, rat.of_nat_div H, of_rat_divide]
+
 end real
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index d24d08eb6..857008868 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -669,7 +669,6 @@ theorem not_lt_self (s : seq) : ¬ s_lt s s :=
     apply absurd Hn (rat.not_lt_of_ge (rat.le_of_lt !inv_pos))
   end
 
-
 theorem not_sep_self (s : seq) : ¬ s ≢ s :=
   begin
     intro Hsep,
@@ -738,7 +737,6 @@ theorem lt_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu :
     repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
   end)
 
-
 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 :=
   begin
@@ -766,7 +764,6 @@ theorem sep_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu :
     assumption
   end
 
-
 theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
         (Hst : s_lt s t) (Htu : s_le t u) : s_lt s u :=
   begin
@@ -1117,8 +1114,6 @@ section migrate_algebra
 
   definition sub (a b : ℝ) : ℝ := algebra.sub a b
   infix [priority real.prio] - := real.sub
-  definition dvd (a b : ℝ) : Prop := algebra.dvd a b
-  notation [priority real.prio] a ∣ b := real.dvd a b
   definition pow (a : ℝ) (n : ℕ) : ℝ := algebra.pow a n
   notation [priority real.prio] a^n := real.pow a n
   definition nmul (n : ℕ) (a : ℝ) : ℝ := algebra.nmul n a
@@ -1126,26 +1121,91 @@ section migrate_algebra
   definition imul (i : ℤ) (a : ℝ) : ℝ := algebra.imul i a
 
   migrate from algebra with real
-    replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, dvd → dvd, divide → divide,
+    hiding dvd, dvd.elim, dvd.elim_left, dvd.intro, dvd.intro_left, dvd.refl, dvd.trans,
+      dvd_mul_left, dvd_mul_of_dvd_left, dvd_mul_of_dvd_right, dvd_mul_right, dvd_neg_iff_dvd,
+      dvd_neg_of_dvd, dvd_of_dvd_neg, dvd_of_mul_left_dvd, dvd_of_mul_left_eq,
+      dvd_of_mul_right_dvd, dvd_of_mul_right_eq, dvd_of_neg_dvd, dvd_sub, dvd_zero
+    replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, divide → divide,
               pow → pow, nmul → nmul, imul → imul
 
   attribute le.trans lt.trans lt_of_lt_of_le lt_of_le_of_lt ge.trans gt.trans gt_of_gt_of_ge
                    gt_of_ge_of_gt [trans]
 end migrate_algebra
 
-theorem of_rat_le_of_rat_of_le (a b : ℚ) : a ≤ b → of_rat a ≤ of_rat b :=
+theorem of_rat_sub (a b : ℚ) : of_rat (a - b) = of_rat a - of_rat b := rfl
+
+theorem of_int_sub (a b : ℤ) : of_int (#int a - b) = of_int a - of_int b :=
+  by rewrite [of_int_eq, rat.of_int_sub, of_rat_sub]
+
+theorem of_rat_le_of_rat_of_le {a b : ℚ} : a ≤ b → of_rat a ≤ of_rat b :=
   rat_seq.r_const_le_const_of_le
 
-theorem le_of_rat_le_of_rat (a b : ℚ) : of_rat a ≤ of_rat b → a ≤ b :=
+theorem le_of_of_rat_le_of_rat {a b : ℚ} : of_rat a ≤ of_rat b → a ≤ b :=
   rat_seq.r_le_of_const_le_const
 
-theorem of_rat_lt_of_rat_of_lt (a b : ℚ) : a < b → of_rat a < of_rat b :=
+theorem of_rat_le_of_rat_iff (a b : ℚ) : of_rat a ≤ of_rat b ↔ a ≤ b :=
+  iff.intro le_of_of_rat_le_of_rat of_rat_le_of_rat_of_le
+
+theorem of_rat_lt_of_rat_of_lt {a b : ℚ} : a < b → of_rat a < of_rat b :=
   rat_seq.r_const_lt_const_of_lt
 
-theorem lt_of_rat_lt_of_rat (a b : ℚ) : of_rat a < of_rat b → a < b :=
+theorem lt_of_of_rat_lt_of_rat {a b : ℚ} : of_rat a < of_rat b → a < b :=
   rat_seq.r_lt_of_const_lt_const
 
-theorem of_rat_sub (a b : ℚ) : of_rat a - of_rat b = of_rat (a - b) := rfl
+theorem of_rat_lt_of_rat_iff (a b : ℚ) : of_rat a < of_rat b ↔ a < b :=
+  iff.intro lt_of_of_rat_lt_of_rat of_rat_lt_of_rat_of_lt
+
+theorem of_int_le_of_int_iff (a b : ℤ) : of_int a ≤ of_int b ↔ (#int a ≤ b) :=
+  by rewrite [*of_int_eq, of_rat_le_of_rat_iff, rat.of_int_le_of_int_iff]
+
+theorem of_int_le_of_int_of_le {a b : ℤ} : (#int a ≤ b) → of_int a ≤ of_int b :=
+  iff.mpr !of_int_le_of_int_iff
+
+theorem le_of_of_int_le_of_int {a b : ℤ} : of_int a ≤ of_int b → (#int a ≤ b) :=
+  iff.mp !of_int_le_of_int_iff
+
+theorem of_int_lt_of_int_iff (a b : ℤ) : of_int a < of_int b ↔ (#int a < b) :=
+  by rewrite [*of_int_eq, of_rat_lt_of_rat_iff, rat.of_int_lt_of_int_iff]
+
+theorem of_int_lt_of_int_of_lt {a b : ℤ} : (#int a < b) → of_int a < of_int b :=
+  iff.mpr !of_int_lt_of_int_iff
+
+theorem lt_of_of_int_lt_of_int {a b : ℤ} : of_int a < of_int b → (#int a < b) :=
+  iff.mp !of_int_lt_of_int_iff
+
+theorem of_nat_le_of_nat_iff (a b : ℕ) : of_nat a ≤ of_nat b ↔ (#nat a ≤ b) :=
+  by rewrite [*of_nat_eq, of_rat_le_of_rat_iff, rat.of_nat_le_of_nat_iff]
+
+theorem of_nat_le_of_nat_of_le {a b : ℕ} : (#nat a ≤ b) → of_nat a ≤ of_nat b :=
+  iff.mpr !of_nat_le_of_nat_iff
+
+theorem le_of_of_nat_le_of_nat {a b : ℕ} : of_nat a ≤ of_nat b → (#nat a ≤ b) :=
+  iff.mp !of_nat_le_of_nat_iff
+
+theorem of_nat_lt_of_nat_iff (a b : ℕ) : of_nat a < of_nat b ↔ (#nat a < b) :=
+  by rewrite [*of_nat_eq, of_rat_lt_of_rat_iff, rat.of_nat_lt_of_nat_iff]
+
+theorem of_nat_lt_of_nat_of_lt {a b : ℕ} : (#nat a < b) → of_nat a < of_nat b :=
+  iff.mpr !of_nat_lt_of_nat_iff
+
+theorem lt_of_of_nat_lt_of_nat {a b : ℕ} : of_nat a < of_nat b → (#nat a < b) :=
+  iff.mp !of_nat_lt_of_nat_iff
+
+theorem of_nat_nonneg (a : ℕ) : of_nat a ≥ 0 :=
+of_rat_le_of_rat_of_le !rat.of_nat_nonneg
+
+theorem of_rat_pow (a : ℚ) (n : ℕ) : of_rat (a^n) = (of_rat a)^n :=
+begin
+  induction n with n ih,
+    apply eq.refl,
+  rewrite [pow_succ, rat.pow_succ, of_rat_mul, ih]
+end
+
+theorem of_int_pow (a : ℤ) (n : ℕ) : of_int (#int a^n) = (of_int a)^n :=
+by rewrite [of_int_eq, rat.of_int_pow, of_rat_pow]
+
+theorem of_nat_pow (a : ℕ) (n : ℕ) : of_nat (#nat a^n) = (of_nat a)^n :=
+by rewrite [of_nat_eq, rat.of_nat_pow, of_rat_pow]
 
 open rat_seq
 theorem le_of_le_reprs (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, x ≤ t n) →
@@ -1155,7 +1215,6 @@ theorem le_of_le_reprs (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, x 
       have H' : ∀ n : ℕ+, r_le s (r_const (t n)), from Hs,
       by apply r_le_of_le_reprs; apply Hs)
 
-
 theorem le_of_reprs_le (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, t n ≤ x) →
         quot.mk (reg_seq.mk t Ht) ≤ x :=
   quot.induction_on x (take s Hs,
diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean
index 4368cf19a..11ad148bd 100644
--- a/library/theories/number_theory/irrational_roots.lean
+++ b/library/theories/number_theory/irrational_roots.lean
@@ -81,7 +81,7 @@ section
     using this, by rewrite [-int.abs_pow, this, int.abs_mul, int.abs_pow],
   have H₁ : (nat_abs a)^n = nat_abs c * (nat_abs b)^n,
     using this,
-      by apply int.of_nat.inj; rewrite [int.of_nat_mul, +of_nat_pow, +of_nat_nat_abs]; assumption,
+      by apply int.of_nat.inj; rewrite [int.of_nat_mul, +int.of_nat_pow, +of_nat_nat_abs]; assumption,
   have H₂ : nat.coprime (nat_abs a) (nat_abs b), from of_nat.inj !coprime_num_denom,
   have nat_abs b = 1, from
     by_cases