diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean
index b57fd34de..11f95f4c5 100644
--- a/library/algebra/group_power.lean
+++ b/library/algebra/group_power.lean
@@ -30,10 +30,10 @@ definition pow_int {A : Type} [s : has_pow_int A] : A → int → A :=
 has_pow_int.pow_int
 
 namespace algebra
-/- monoid -/
-
+ /- monoid -/
 section monoid
 open nat
+
 variable [s : monoid A]
 include s
 
@@ -121,32 +121,33 @@ theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m
 
 end nat
 
-open nat int
+open int
 
 definition gpow (a : A) : ℤ → A
 | (of_nat n) := a^n
 | -[1+n]     := (a^(nat.succ n))⁻¹
 
-/-
+open nat
+
 private lemma gpow_add_aux (a : A) (m n : nat) :
   gpow a ((of_nat m) + -[1+n]) = gpow a (of_nat m) * gpow a (-[1+n]) :=
 or.elim (nat.lt_or_ge m (nat.succ n))
   (assume H : (m < nat.succ n),
-    assert H1 : (nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H,
+    assert H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H,
     calc
       gpow a ((of_nat m) + -[1+n]) = gpow a (sub_nat_nat m (nat.succ n))  : rfl
-        ... = gpow a (-[1+ nat.pred (sub (nat.succ n) m)])            : {sub_nat_nat_of_lt H}
-        ... = (pow a (nat.succ (nat.pred (sub (nat.succ n) m))))⁻¹    : rfl
-        ... = (pow a (nat.succ n) * (pow a m)⁻¹)⁻¹                        :
-                by rewrite [succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)]
-        ... = pow a m * (pow a (nat.succ n))⁻¹                            :
+        ... = gpow a (-[1+ nat.pred (nat.sub (nat.succ n) m)])            : {sub_nat_nat_of_lt H}
+        ... = (a ^ (nat.succ (nat.pred (nat.sub (nat.succ n) m))))⁻¹    : rfl
+        ... = (a ^ (nat.succ n) * (a ^ m)⁻¹)⁻¹                        :
+                by krewrite [succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)]
+        ... = a ^ m * (a ^ (nat.succ n))⁻¹                            :
                 by rewrite [mul_inv, inv_inv]
         ... = gpow a (of_nat m) * gpow a (-[1+n])                         : rfl)
-  (assume H : (#nat m ≥ nat.succ n),
+  (assume H : (m ≥ nat.succ n),
     calc
       gpow a ((of_nat m) + -[1+n]) = gpow a (sub_nat_nat m (nat.succ n))  : rfl
         ... = gpow a (#nat m - nat.succ n)                                : {sub_nat_nat_of_ge H}
-        ... = pow a m * (pow a (nat.succ n))⁻¹                            : pow_sub a H
+        ... = a ^ m * (a ^ (nat.succ n))⁻¹                                : pow_sub a H
         ... = gpow a (of_nat m) * gpow a (-[1+n])                         : rfl)
 
 theorem gpow_add (a : A) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j
@@ -161,15 +162,14 @@ theorem gpow_add (a : A) : ∀i j : int, gpow a (i + j) = gpow a i * gpow a j
 
 theorem gpow_comm (a : A) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a i :=
 by rewrite [-*gpow_add, int.add.comm]
--/
 end group
-/-
+
 section ordered_ring
 open nat
 variable [s : linear_ordered_ring A]
 include s
 
-theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : pow a n > 0 :=
+theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : a ^ n > 0 :=
   begin
     induction n,
     rewrite pow_zero,
@@ -179,12 +179,12 @@ theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : pow a n > 0 :=
     apply v_0, apply H
   end
 
-theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : pow a n ≥ 1 :=
+theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : a ^ n ≥ 1 :=
   begin
     induction n,
     rewrite pow_zero,
     apply le.refl,
-    rewrite [pow_succ', -{1}mul_one],
+    rewrite [pow_succ', -mul_one 1],
     apply mul_le_mul v_0 H zero_le_one,
     apply le_of_lt,
     apply pow_pos,
@@ -193,7 +193,7 @@ theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : pow a n ≥ 1 :=
 
 local notation 2 := (1 : A) + 1
 
-theorem pow_two_add (n : ℕ) : pow 2 n + pow 2 n = pow 2 (succ n) :=
+theorem pow_two_add (n : ℕ) : 2^n + 2^n = 2^(succ n) :=
   by rewrite [pow_succ', left_distrib, *mul_one]
 
 end ordered_ring
@@ -206,7 +206,7 @@ include s
 local attribute add_monoid.to_monoid [trans-instance]
 open nat
 
-definition nmul : ℕ → A → A := λ n a, pow a n
+definition nmul : ℕ → A → A := λ n a, a^n
 
 infix [priority algebra.prio] `⬝` := nmul
 
@@ -264,6 +264,5 @@ theorem add_imul (i j : ℤ) (a : A) : imul (i + j) a = imul i a + imul j a :=
 theorem imul_comm (i j : ℤ) (a : A) : imul i a + imul j a = imul j a + imul i a := gpow_comm a i j
 
 end add_group
--/
 
 end algebra
diff --git a/library/data/bag.lean b/library/data/bag.lean
index e3a6fa5b4..9379ae949 100644
--- a/library/data/bag.lean
+++ b/library/data/bag.lean
@@ -8,6 +8,7 @@ Finite bags.
 import data.nat data.list.perm algebra.binary
 open nat quot list subtype binary function eq.ops
 open [declarations] perm
+open - [notations] algebra
 
 variable {A : Type}
 
diff --git a/library/data/fin.lean b/library/data/fin.lean
index 78f8f2970..6db7c7c3d 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -7,6 +7,7 @@ Finite ordinal types.
 -/
 import data.list.basic data.finset.basic data.fintype.card algebra.group data.equiv
 open eq.ops nat function list finset fintype
+open - [notations] algebra
 
 structure fin (n : nat) := (val : nat) (is_lt : val < n)
 
@@ -149,7 +150,7 @@ take i j, destruct i (destruct j (take iv ilt jv jlt Pmkeq,
   begin congruence, apply fin.no_confusion Pmkeq, intros, assumption end))
 
 lemma lt_of_inj_of_max (f : fin (succ n) → fin (succ n)) :
-  injective f → (f maxi = maxi) → ∀ i, i < n → f i < n :=
+  injective f → (f maxi = maxi) → ∀ i : fin (succ n), i < n → f i < n :=
 assume Pinj Peq, take i, assume Pilt,
 assert P1 : f i = f maxi → i = maxi, from assume Peq, Pinj i maxi Peq,
 have f i ≠ maxi, from
@@ -399,7 +400,7 @@ definition fin_sum_equiv (n m : nat) : (fin n + fin m) ≃ fin (n+m) :=
 assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from
   take v, suppose v < m, calc
      v + n < m + n   : add_lt_add_of_lt_of_le this !le.refl
-       ... = n + m  : add.comm,
+       ... = n + m   : algebra.add.comm,
 ⦃ equiv,
   to_fun := λ s : sum (fin n) (fin m),
     match s with
diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean
index 78cff73e3..665da3a09 100644
--- a/library/data/finset/card.lean
+++ b/library/data/finset/card.lean
@@ -7,6 +7,7 @@ Cardinality calculations for finite sets.
 -/
 import .to_set .bigops data.set.function data.nat.power data.nat.bigops
 open nat nat.finset eq.ops
+open - [notations] algebra
 
 namespace finset
 
@@ -42,7 +43,7 @@ end
 
 theorem card_union (s₁ s₂ : finset A) : card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) :=
 calc
-  card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : add_sub_cancel
+  card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : nat.add_sub_cancel
              ... = card s₁ + card s₂ - card (s₁ ∩ s₂)               : card_add_card
 
 theorem card_union_of_disjoint {s₁ s₂ : finset A} (H : s₁ ∩ s₂ = ∅) :
diff --git a/library/data/finset/equiv.lean b/library/data/finset/equiv.lean
index 2de7a0bf6..a80d2e094 100644
--- a/library/data/finset/equiv.lean
+++ b/library/data/finset/equiv.lean
@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 import data.finset.card
 open nat nat.finset decidable
+open - [notations] algebra
 
 namespace finset
 variable {A : Type}
@@ -57,7 +58,7 @@ iff.intro
 
 private lemma odd_of_zero_mem (s : nat) : 0 ∈ of_nat s ↔ odd s :=
 begin
-  unfold of_nat, rewrite [mem_sep_eq, pow_zero, div_one, mem_upto_eq],
+  unfold of_nat, krewrite [mem_sep_eq, pow_zero, div_one, mem_upto_eq],
   show 0 < succ s ∧ odd s ↔ odd s, from
   iff.intro
     (assume h, and.right h)
diff --git a/library/data/hf.lean b/library/data/hf.lean
index c07956b5b..88d16e82d 100644
--- a/library/data/hf.lean
+++ b/library/data/hf.lean
@@ -11,7 +11,8 @@ this bijection is implemeted using the Ackermann coding.
 -/
 import data.nat data.finset.equiv data.list
 open nat binary
-open -[notations]finset
+open -[notations] finset
+open -[notations] algebra
 
 definition hf := nat
 
@@ -23,7 +24,7 @@ protected definition prio : num := num.succ std.priority.default
 protected definition is_inhabited [instance] : inhabited hf :=
 nat.is_inhabited
 
-protected definition has_decidable_eq [instance] : decidable_eq hf :=
+protected definition has_decidable_eq [reducible] [instance] : decidable_eq hf :=
 nat.has_decidable_eq
 
 definition of_finset (s : finset hf) : hf :=
@@ -71,7 +72,8 @@ lemma insert_lt_of_not_mem {a s : hf} : a ∉ s → s < insert a s :=
 begin
   unfold [insert, of_finset, equiv.to_fun, finset_nat_equiv_nat, mem, to_finset, equiv.inv],
   intro h,
-  krewrite [finset.to_nat_insert h, to_nat_of_nat, -zero_add s at {1}],
+  rewrite [finset.to_nat_insert h],
+  rewrite [to_nat_of_nat, -zero_add s at {1}],
   apply add_lt_add_right,
   apply pow_pos_of_pos _ dec_trivial
 end
@@ -81,7 +83,8 @@ lemma insert_lt_insert_of_not_mem_of_not_mem_of_lt {a s₁ s₂ : hf}
 begin
   unfold [insert, of_finset, equiv.to_fun, finset_nat_equiv_nat, mem, to_finset, equiv.inv],
   intro h₁ h₂ h₃,
-  krewrite [finset.to_nat_insert h₁, finset.to_nat_insert h₂, *to_nat_of_nat],
+  rewrite [finset.to_nat_insert h₁],
+  rewrite [finset.to_nat_insert h₂, *to_nat_of_nat],
   apply add_lt_add_left h₃
 end
 
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index bda043007..06231f3fc 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -528,12 +528,15 @@ has_sub.mk algebra.sub
 definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int :=
 has_dvd.mk algebra.dvd
 
+set_option pp.coercions true
+
 /- additional properties -/
-theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : m - n = sub m n :=
+theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : of_nat (m - n) = of_nat m - of_nat n :=
 assert m - n + n = m,     from nat.sub_add_cancel H,
 begin
   symmetry,
-  apply sub_eq_of_eq_add,
+  apply algebra.sub_eq_of_eq_add,
+  rewrite -of_nat_add,
   rewrite this
 end
 
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index e23d5e5c0..11313c974 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -38,11 +38,15 @@ protected definition modulo (a b : ℤ) : ℤ := a - a div b * b
 definition int_has_modulo [reducible] [instance] [priority int.prio] : has_modulo int :=
 has_modulo.mk int.modulo
 
+
+lemma modulo.def (a b : ℤ) : a mod b = a - a div b * b :=
+rfl
+
 notation [priority int.prio] a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c
 
 /- div  -/
 
-theorem of_nat_div (m n : nat) : of_nat (m div n) = m div n :=
+theorem of_nat_div (m n : nat) : of_nat (m div n) = (of_nat m) div (of_nat n) :=
 nat.cases_on n
   (begin krewrite [divide_of_nat, sign_zero, zero_mul, nat.div_zero] end)
   (take (n : nat), by krewrite [divide_of_nat, sign_of_succ, one_mul])
@@ -256,7 +260,7 @@ theorem div_self {a : ℤ} (H : a ≠ 0) : a div a = 1 :=
 
 /- mod -/
 
-theorem of_nat_mod (m n : nat) : m mod n = (#nat m mod n) :=
+theorem of_nat_mod (m n : nat) : (of_nat m) mod (of_nat n) = of_nat (m mod n) :=
 sorry
 /-
 have H : m = (#nat m mod n) + m div n * n, from calc
diff --git a/library/data/list/sort.lean b/library/data/list/sort.lean
index 81981b32e..8ea633969 100644
--- a/library/data/list/sort.lean
+++ b/library/data/list/sort.lean
@@ -178,10 +178,10 @@ eq_of_sorted_of_perm tr asy p s₁ s₂
 section
 open algebra
 omit decR
-lemma strongly_sorted_sort [ord : decidable_linear_order A] (l : list A) : strongly_sorted has_le.le (sort has_le.le l) :=
+lemma strongly_sorted_sort [ord : decidable_linear_order A] (l : list A) : strongly_sorted le (sort le l) :=
 strongly_sorted_sort_core le.total (@le.trans A ord) le.refl l
 
-lemma sort_eq_of_perm {l₁ l₂ : list A} [ord : decidable_linear_order A] (h : l₁ ~ l₂) : sort has_le.le l₁ = sort has_le.le l₂ :=
+lemma sort_eq_of_perm {l₁ l₂ : list A} [ord : decidable_linear_order A] (h : l₁ ~ l₂) : sort le l₁ = sort le l₂ :=
 sort_eq_of_perm_core le.total (@le.trans A ord) le.refl (@le.antisymm A ord) h
 end
 end list
diff --git a/library/data/matrix.lean b/library/data/matrix.lean
index 3067891ae..d8910f0db 100644
--- a/library/data/matrix.lean
+++ b/library/data/matrix.lean
@@ -53,26 +53,35 @@ definition identity (n : nat) : matrix A n n :=
 definition I {n : nat} : matrix A n n :=
 identity n
 
-definition zero (m n : nat) : matrix A m n :=
+protected definition zero (m n : nat) : matrix A m n :=
 λ i j, 0
 
-definition add (M : matrix A m n) (N : matrix A m n) : matrix A m n :=
+protected definition add (M : matrix A m n) (N : matrix A m n) : matrix A m n :=
 λ i j, M[i, j] + N[i, j]
 
-definition sub (M : matrix A m n) (N : matrix A m n) : matrix A m n :=
+protected definition sub (M : matrix A m n) (N : matrix A m n) : matrix A m n :=
 λ i j, M[i, j] - N[i, j]
 
+protected definition mul (M : matrix A m n) (N : matrix A n p) : matrix A m p :=
+λ i j, fin.foldl has_add.add 0 (λ k : fin n, M[i,k] * N[k,j])
+
 definition smul (a : A) (M : matrix A m n) : matrix A m n :=
 λ i j, a * M[i, j]
 
-definition mul (M : matrix A m n) (N : matrix A n p) : matrix A m p :=
-λ i j, fin.foldl has_add.add 0 (λ k : fin n, M[i,k] * N[k,j])
+definition matrix_has_zero [reducible] [instance] (m n : nat) : has_zero (matrix A m n) :=
+has_zero.mk (matrix.zero m n)
 
-infix + := add
-infix - := sub
-infix * := mul
-infix * := smul
-notation 0 := zero _ _
+definition matrix_has_one [reducible] [instance] (n : nat) : has_one (matrix A n n) :=
+has_one.mk (identity n)
+
+definition matrix_has_add [reducible] [instance] (m n : nat) : has_add (matrix A m n) :=
+has_add.mk matrix.add
+
+definition matrix_has_mul [reducible] [instance] (n : nat) : has_mul (matrix A n n) :=
+has_mul.mk matrix.mul
+
+infix ` × ` := mul
+infix `⬝`    := smul
 
 lemma add_zero (M : matrix A m n) : M + 0 = M :=
 matrix.ext (λ i j, !algebra.add_zero)
@@ -93,10 +102,10 @@ definition is_zero (M : matrix A m n) :=
 ∀ i j, M[i, j] = 0
 
 definition is_upper_triangular (M : matrix A n n) :=
-∀ i j, i > j → M[i, j] = 0
+∀ i j : fin n, i > j → M[i, j] = 0
 
 definition is_lower_triangular (M : matrix A n n) :=
-∀ i j, i < j → M[i, j] = 0
+∀ i j : fin n, i < j → M[i, j] = 0
 
 definition inverse (M : matrix A n n) (N : matrix A n n) :=
 M * N = I ∧ N * M = I
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 00f62ab2e..697917c26 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -83,8 +83,7 @@ theorem mul_le_mul {n m k l : ℕ} (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k *
 le.trans (!mul_le_mul_right H1) (!mul_le_mul_left H2)
 
 theorem mul_lt_mul_of_pos_left {n m k : ℕ} (H : n < m) (Hk : k > 0) : k * n < k * m :=
-calc k * n < k * n + k : lt_add_of_pos_right Hk
-      ...  ≤ k * m     : !mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H)
+lt_of_lt_of_le (lt_add_of_pos_right Hk) (!mul_succ ▸ mul_le_mul_left k (succ_le_of_lt H))
 
 theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
 !mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index b1cea8b2e..12bd48df9 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -7,6 +7,7 @@ The rational numbers as a field generated by the integers, defined as the usual
 -/
 import data.int algebra.field
 open int quot eq.ops
+open - [notations] algebra
 
 record prerat : Type :=
 (num : ℤ) (denom : ℤ) (denom_pos : denom > 0)
@@ -39,13 +40,14 @@ have num b * denom a > 0, from H ▸ this,
 show num b > 0, from pos_of_mul_pos_right this (le_of_lt (denom_pos a))
 
 theorem num_neg_of_equiv {a b : prerat} (H : a ≡ b) (na_neg : num a < 0) : num b < 0 :=
-have num a * denom b < 0, from mul_neg_of_neg_of_pos na_neg (denom_pos b),
-have -(-num b * denom a) < 0, from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_neg⁻¹ ▸ H ▸ this,
+assert H₁ : num a * denom b = num b * denom a, from H,
+assert num a * denom b < 0,     from mul_neg_of_neg_of_pos na_neg (denom_pos b),
+have -(-num b * denom a) < 0,   begin rewrite [neg_mul_eq_neg_mul, neg_neg, -H₁], exact this end,
 have -num b > 0, from pos_of_mul_pos_right (pos_of_neg_neg this) (le_of_lt (denom_pos a)),
 neg_of_neg_pos this
 
 theorem equiv_of_num_eq_zero {a b : prerat} (H1 : num a = 0) (H2 : num b = 0) : a ≡ b :=
-by rewrite [↑equiv, H1, H2, *zero_mul]
+by krewrite [↑equiv, H1, H2, *zero_mul]
 
 theorem equiv.trans [trans] {a b c : prerat} (H1 : a ≡ b) (H2 : b ≡ c) : a ≡ c :=
 decidable.by_cases
@@ -95,13 +97,13 @@ prerat.mk (- num a) (denom a) (denom_pos a)
 definition smul (a : ℤ) (b : prerat) (H : a > 0) : prerat :=
 prerat.mk (a * num b) (a * denom b) (mul_pos H (denom_pos b))
 
-theorem of_int_add (a b : ℤ) : of_int (#int a + b) ≡ add (of_int a) (of_int b) :=
+theorem of_int_add (a b : ℤ) : of_int (a + b) ≡ add (of_int a) (of_int b) :=
 by esimp [equiv, num, denom, one, add, of_int]; rewrite [*int.mul_one]
 
-theorem of_int_mul (a b : ℤ) : of_int (#int a * b) ≡ mul (of_int a) (of_int b) :=
+theorem of_int_mul (a b : ℤ) : of_int (a * b) ≡ mul (of_int a) (of_int b) :=
 !equiv.refl
 
-theorem of_int_neg (a : ℤ) : of_int (#int -a) ≡ neg (of_int a) :=
+theorem of_int_neg (a : ℤ) : of_int (-a) ≡ neg (of_int a) :=
 !equiv.refl
 
 theorem of_int.inj {a b : ℤ} : of_int a ≡ of_int b → a = b :=
@@ -113,26 +115,28 @@ definition inv : prerat → prerat
 | inv (prerat.mk -[1+n] d dp)       := prerat.mk (-d) (nat.succ n) !of_nat_succ_pos
 
 theorem equiv_zero_of_num_eq_zero {a : prerat} (H : num a = 0) : a ≡ zero :=
-by rewrite [↑equiv, H, ↑zero, ↑num, ↑of_int, *zero_mul]
+by krewrite [↑equiv, H, ↑zero, ↑num, ↑of_int, *zero_mul]
 
 theorem num_eq_zero_of_equiv_zero {a : prerat} : a ≡ zero → num a = 0 :=
-by rewrite [↑equiv, ↑zero, ↑of_int, mul_one, zero_mul]; intro H; exact H
+by krewrite [↑equiv, ↑zero, ↑of_int, mul_one, zero_mul]; intro H; exact H
 
 theorem inv_zero {d : int} (dp : d > 0) : inv (mk nat.zero d dp) = zero :=
 begin rewrite [↑inv, ▸*] end
 
 theorem inv_zero' : inv zero = zero := inv_zero (of_nat_succ_pos nat.zero)
 
+open nat
+
 theorem inv_of_pos {n d : int} (np : n > 0) (dp : d > 0) : inv (mk n d dp) ≡ mk d n np :=
 obtain (n' : nat) (Hn' : n = of_nat n'), from exists_eq_of_nat (le_of_lt np),
-have (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
+have (n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
 obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt this,
 have d * n = d * nat.succ k, by rewrite [Hn', Hk],
 Hn'⁻¹ ▸ (Hk⁻¹ ▸ this)
 
 theorem inv_neg {n d : int} (np : n > 0) (dp : d > 0) : inv (mk (-n) d dp) ≡ mk (-d) n np :=
 obtain (n' : nat) (Hn' : n = of_nat n'), from exists_eq_of_nat (le_of_lt np),
-have (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
+have (n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
 obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt this,
 have -d * n = -d * nat.succ k, by rewrite [Hn', Hk],
 have H3 : inv (mk -[1+k] d dp) ≡ mk (-d) n np, from this,
@@ -215,10 +219,10 @@ by rewrite [↑add, ↑equiv, ▸*, *(mul.comm (num c)), *(λy, mul.comm y (deno
             *mul.right_distrib, *mul.assoc, *add.assoc]
 
 theorem add_zero (a : prerat) : add a zero ≡ a :=
-by rewrite [↑add, ↑equiv, ↑zero, ↑of_int, ▸*, *mul_one, zero_mul, add_zero]
+by krewrite [↑add, ↑equiv, ↑zero, ↑of_int, ▸*, *mul_one, zero_mul, add_zero]
 
 theorem add.left_inv (a : prerat) : add (neg a) a ≡ zero :=
-by rewrite [↑add, ↑equiv, ↑neg, ↑zero, ↑of_int, ▸*, -neg_mul_eq_neg_mul, add.left_inv, *zero_mul]
+by krewrite [↑add, ↑equiv, ↑neg, ↑zero, ↑of_int, ▸*, -neg_mul_eq_neg_mul, add.left_inv, *zero_mul]
 
 theorem mul.comm (a b : prerat) : mul a b ≡ mul b a :=
 by rewrite [↑mul, ↑equiv, mul.comm (num a), mul.comm (denom a)]
@@ -269,7 +273,7 @@ theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ on
 theorem zero_not_equiv_one : ¬ zero ≡ one :=
 begin
   esimp [equiv, zero, one, of_int],
-  rewrite [zero_mul, int.mul_one],
+  krewrite [zero_mul, int.mul_one],
   exact zero_ne_one
 end
 
@@ -309,14 +313,14 @@ theorem reduce_eq_reduce : ∀{a b : prerat}, a ≡ b → reduce a = reduce b
   assume H : an * bd = bn * ad,
   decidable.by_cases
     (assume anz : an = 0,
-      have H' : bn * ad = 0, by rewrite [-H, anz, zero_mul],
+      have H' : bn * ad = 0, by krewrite [-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 H' : an * bd = 0, by krewrite [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,
@@ -352,22 +356,22 @@ definition of_int [coercion] (i : ℤ) : ℚ := ⟦prerat.of_int i⟧
 definition of_nat [coercion] (n : ℕ) : ℚ := nat.to.rat n
 definition of_num [coercion] [reducible] (n : num) : ℚ := num.to.rat n
 
-definition add : ℚ → ℚ → ℚ :=
+protected definition add : ℚ → ℚ → ℚ :=
 quot.lift₂
   (λ 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 : ℚ → ℚ → ℚ :=
+protected definition mul : ℚ → ℚ → ℚ :=
 quot.lift₂
   (λ 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 : ℚ → ℚ :=
+protected definition neg : ℚ → ℚ :=
 quot.lift
   (λ a : prerat, ⟦prerat.neg a⟧)
   (take a1 a2, assume H, quot.sound (prerat.neg_equiv_neg H))
 
-definition inv : ℚ → ℚ :=
+protected definition inv : ℚ → ℚ :=
 quot.lift
   (λ a : prerat, ⟦prerat.inv a⟧)
   (take a1 a2, assume H, quot.sound (prerat.inv_equiv_inv H))
@@ -385,30 +389,41 @@ prerat.denom_pos (reduce a)
 
 protected definition prio := num.pred int.prio
 
-infix [priority rat.prio] +    := rat.add
-infix [priority rat.prio] *    := rat.mul
-prefix [priority rat.prio] -   := rat.neg
+definition rat_has_add [reducible] [instance] [priority rat.prio] : has_add rat :=
+has_add.mk rat.add
 
-definition sub [reducible] (a b : rat) : rat := a + (-b)
+definition rat_has_mul [reducible] [instance] [priority rat.prio] : has_mul rat :=
+has_mul.mk rat.mul
 
-postfix [priority rat.prio] ⁻¹ := rat.inv
-infix [priority rat.prio] -    := rat.sub
+definition rat_has_neg [reducible] [instance] [priority rat.prio] : has_neg rat :=
+has_neg.mk rat.neg
+
+definition rat_has_inv [reducible] [instance] [priority rat.prio] : has_inv rat :=
+has_inv.mk rat.inv
+
+protected definition sub [reducible] (a b : ℚ) : rat := a + (-b)
+
+definition rat_has_sub [reducible] [instance] [priority rat.prio] : has_sub rat :=
+has_sub.mk rat.sub
+
+lemma sub.def (a b : ℚ) : a - b = a + (-b) :=
+rfl
 
 /- properties -/
 
-theorem of_int_add (a b : ℤ) : of_int (#int a + b) = of_int a + of_int b :=
+theorem of_int_add (a b : ℤ) : of_int (a + b) = of_int a + of_int b :=
 quot.sound (prerat.of_int_add a b)
 
-theorem of_int_mul (a b : ℤ) : of_int (#int a * b) = of_int a * of_int b :=
+theorem of_int_mul (a b : ℤ) : of_int (a * b) = of_int a * of_int b :=
 quot.sound (prerat.of_int_mul a b)
 
-theorem of_int_neg (a : ℤ) : of_int (#int -a) = -(of_int a) :=
+theorem of_int_neg (a : ℤ) : of_int (-a) = -(of_int a) :=
 quot.sound (prerat.of_int_neg a)
 
-theorem of_int_sub (a b : ℤ) : of_int (#int a - b) = of_int a - of_int b :=
+theorem of_int_sub (a b : ℤ) : of_int (a - b) = of_int a - of_int b :=
 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}
+  of_int (a - b) = of_int a + of_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 :=
 prerat.of_int.inj (quot.exact H)
@@ -416,16 +431,23 @@ prerat.of_int.inj (quot.exact 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_nat_eq (a : ℕ) : of_nat a = of_int (int.of_nat a) := rfl
+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 :=
+open nat
+
+theorem of_nat_add (a b : ℕ) : of_nat (a + b) = of_nat a + of_nat b :=
 by rewrite [of_nat_eq, int.of_nat_add, rat.of_int_add]
 
-theorem of_nat_mul (a b : ℕ) : of_nat (#nat a * b) = of_nat a * of_nat b :=
+theorem of_nat_mul (a b : ℕ) : of_nat (a * b) = of_nat a * of_nat b :=
 by rewrite [of_nat_eq, int.of_nat_mul, rat.of_int_mul]
 
-theorem of_nat_sub {a b : ℕ} (H : #nat a ≥ b) : of_nat (#nat a - b) = of_nat a - of_nat b :=
-by rewrite [of_nat_eq, int.of_nat_sub H, rat.of_int_sub]
+theorem of_nat_sub {a b : ℕ} (H : a ≥ b) : of_nat (a - b) = of_nat a - of_nat b :=
+begin
+  rewrite of_nat_eq,
+  rewrite [int.of_nat_sub H],
+  rewrite [rat.of_int_sub]
+end
 
 theorem of_nat.inj {a b : ℕ} (H : of_nat a = of_nat b) : a = b :=
 int.of_nat.inj (of_int.inj H)
@@ -492,9 +514,12 @@ 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)
 
+section
+local attribute rat [reducible]
 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
+end
 
 theorem coprime_num_denom (a : ℚ) : coprime (num a) (denom a) :=
 decidable.by_cases
@@ -509,81 +534,65 @@ decidable.by_cases
         apply coprime_div_gcd_div_gcd this
       end))
 
-section migrate_algebra
-  open [classes] algebra
 
-  protected definition discrete_field [reducible] : algebra.discrete_field rat :=
-  ⦃algebra.discrete_field,
-    add              := add,
-    add_assoc        := add.assoc,
-    zero             := 0,
-    zero_add         := zero_add,
-    add_zero         := add_zero,
-    neg              := neg,
-    add_left_inv     := add.left_inv,
-    add_comm         := add.comm,
-    mul              := mul,
-    mul_assoc        := mul.assoc,
-    one              := 1,
-    one_mul          := one_mul,
-    mul_one          := mul_one,
-    left_distrib     := mul.left_distrib,
-    right_distrib    := mul.right_distrib,
-    mul_comm         := mul.comm,
-    mul_inv_cancel   := @mul_inv_cancel,
-    inv_mul_cancel   := @inv_mul_cancel,
-    zero_ne_one      := zero_ne_one,
-    inv_zero         := inv_zero,
-    has_decidable_eq := has_decidable_eq⦄
+protected definition discrete_field [reducible] [instance] : algebra.discrete_field rat :=
+⦃algebra.discrete_field,
+ add              := rat.add,
+ add_assoc        := add.assoc,
+ zero             := 0,
+ zero_add         := zero_add,
+ add_zero         := add_zero,
+ neg              := rat.neg,
+ add_left_inv     := add.left_inv,
+ add_comm         := add.comm,
+ mul              := rat.mul,
+ mul_assoc        := mul.assoc,
+ one              := 1,
+ one_mul          := one_mul,
+ mul_one          := mul_one,
+ left_distrib     := mul.left_distrib,
+ right_distrib    := mul.right_distrib,
+ mul_comm         := mul.comm,
+ mul_inv_cancel   := @mul_inv_cancel,
+ inv_mul_cancel   := @inv_mul_cancel,
+ zero_ne_one      := zero_ne_one,
+ inv_zero         := inv_zero,
+ has_decidable_eq := has_decidable_eq⦄
 
-  local attribute rat.discrete_field [instance]
+definition rat_has_division [instance] [reducible] [priority rat.prio] : has_division rat :=
+has_division.mk algebra.division
 
-  definition divide (a b : rat) := algebra.divide a b
-  infix [priority rat.prio] / := divide
-
-  definition pow (a : ℚ) (n : ℕ) : ℚ := algebra.pow a n
-  infix [priority rat.prio] ^ := pow
-  definition nmul (n : ℕ) (a : ℚ) : ℚ := algebra.nmul n a
-  infix [priority rat.prio] ⬝ := nmul
-  definition imul (i : ℤ) (a : ℚ) : ℚ := algebra.imul i a
-
-  migrate from algebra with rat
-    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
+definition rat_has_pow_nat [instance] [reducible] [priority rat.prio] : has_pow_nat rat :=
+has_pow_nat.mk pow_nat
 
 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 : (#int b ∣ a)) : of_int (a div b) = of_int a / of_int b :=
+theorem of_int_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])
+    by krewrite [bz, div_zero, algebra.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
+      dvd.elim H
         (take c, assume Hc : a = b * c,
           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,
+theorem of_nat_div {a b : ℕ} (H : b ∣ a) : of_nat (a div b) = of_nat a / of_nat b :=
+have H' : (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,
     apply eq.refl,
-  rewrite [pow_succ, int.pow_succ, of_int_mul, ih]
+  krewrite [pow_succ, pow_succ, of_int_mul, ih]
 end
 
-theorem of_nat_pow (a : ℕ) (n : ℕ) : of_nat (#nat a^n) = (of_nat a)^n :=
+theorem of_nat_pow (a : ℕ) (n : ℕ) : of_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 0d534ca71..10c464d90 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -5,9 +5,9 @@ Author: Jeremy Avigad
 
 Adds the ordering, and instantiates the rationals as an ordered field.
 -/
-
-import data.int algebra.ordered_field .basic
+import data.int algebra.ordered_field algebra.group_power data.rat.basic
 open quot eq.ops
+open - [notations] algebra
 
 /- the ordering on representations -/
 
@@ -21,10 +21,10 @@ definition pos (a : prerat) : Prop := num a > 0
 
 definition nonneg (a : prerat) : Prop := num a ≥ 0
 
-theorem pos_of_int (a : ℤ) : pos (of_int a) ↔ (#int a > 0) :=
+theorem pos_of_int (a : ℤ) : pos (of_int a) ↔ (a > 0) :=
 !iff.rfl
 
-theorem nonneg_of_int (a : ℤ) : nonneg (of_int a) ↔ (#int a ≥ 0) :=
+theorem nonneg_of_int (a : ℤ) : nonneg (of_int a) ↔ (a ≥ 0) :=
 !iff.rfl
 
 theorem pos_eq_pos_of_equiv {a b : prerat} (H1 : a ≡ b) : pos a = pos b :=
@@ -85,7 +85,7 @@ local attribute prerat.setoid [instance]
 -/
 
 namespace rat
-
+open nat int
 variables {a b c : ℚ}
 
 /- transfer properties of pos and nonneg -/
@@ -96,10 +96,10 @@ quot.lift prerat.pos @prerat.pos_eq_pos_of_equiv a
 private definition nonneg (a : ℚ) : Prop :=
 quot.lift prerat.nonneg @prerat.nonneg_eq_nonneg_of_equiv a
 
-private theorem pos_of_int (a : ℤ) : (#int a > 0) ↔ pos (of_int a) :=
+private theorem pos_of_int (a : ℤ) : (a > 0) ↔ pos (of_int a) :=
 prerat.pos_of_int a
 
-private theorem nonneg_of_int (a : ℤ) : (#int a ≥ 0) ↔ nonneg (of_int a) :=
+private theorem nonneg_of_int (a : ℤ) : (a ≥ 0) ↔ nonneg (of_int a) :=
 prerat.nonneg_of_int a
 
 private theorem nonneg_zero : nonneg 0 := prerat.nonneg_zero
@@ -140,73 +140,76 @@ quot.rec_on_subsingleton a (take u, int.decidable_lt 0 (prerat.num u))
 
 /- define order in terms of pos and nonneg -/
 
-definition lt (a b : ℚ) : Prop := pos (b - a)
-definition le (a b : ℚ) : Prop := nonneg (b - a)
-definition gt [reducible] (a b : ℚ) := lt b a
-definition ge [reducible] (a b : ℚ) := le b a
+protected definition lt (a b : ℚ) : Prop := pos (b - a)
+protected definition le (a b : ℚ) : Prop := nonneg (b - a)
 
-infix [priority rat.prio] <  := rat.lt
-infix [priority rat.prio] <= := rat.le
-infix [priority rat.prio] ≤  := rat.le
-infix [priority rat.prio] >= := rat.ge
-infix [priority rat.prio] ≥  := rat.ge
-infix [priority rat.prio] >  := rat.gt
+definition rat_has_lt [reducible] [instance] [priority rat.prio] : has_lt rat :=
+has_lt.mk rat.lt
 
-theorem of_int_lt_of_int_iff (a b : ℤ) : of_int a < of_int b ↔ (#int a < b) :=
+definition rat_has_le [reducible] [instance] [priority rat.prio] : has_le rat :=
+has_le.mk rat.le
+
+lemma lt.def (a b : ℚ) : (a < b) = pos (b - a) :=
+rfl
+
+lemma le.def (a b : ℚ) : (a ≤ b) = nonneg (b - a) :=
+rfl
+
+theorem of_int_lt_of_int_iff (a b : ℤ) : of_int a < of_int b ↔ a < b :=
 iff.symm (calc
-  (#int a < b) ↔ (#int b - a > 0)          : iff.symm !int.sub_pos_iff_lt
-           ... ↔ pos (of_int (#int b - a)) : iff.symm !pos_of_int
-           ... ↔ pos (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
-           ... ↔ of_int a < of_int b       : iff.rfl)
+  a < b ↔ b - a > 0                 : iff.symm !sub_pos_iff_lt
+    ... ↔ pos (of_int (b - a))      : iff.symm !pos_of_int
+    ... ↔ pos (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
+    ... ↔ of_int a < of_int b       : iff.rfl)
 
-theorem of_int_lt_of_int_of_lt {a b : ℤ} (H : (#int a < b)) : of_int a < of_int b :=
+theorem of_int_lt_of_int_of_lt {a b : ℤ} (H : a < b) : of_int a < of_int b :=
 iff.mpr !of_int_lt_of_int_iff H
 
-theorem lt_of_of_int_lt_of_int {a b : ℤ} (H : of_int a < of_int b) : (#int a < b) :=
+theorem lt_of_of_int_lt_of_int {a b : ℤ} (H : of_int a < of_int b) : a < b :=
 iff.mp !of_int_lt_of_int_iff H
 
-theorem of_int_le_of_int_iff (a b : ℤ) : of_int a ≤ of_int b ↔ (#int a ≤ b) :=
+theorem of_int_le_of_int_iff (a b : ℤ) : of_int a ≤ of_int b ↔ (a ≤ b) :=
 iff.symm (calc
-  (#int a ≤ b) ↔ (#int b - a ≥ 0)             : iff.symm !int.sub_nonneg_iff_le
-           ... ↔ nonneg (of_int (#int b - a)) : iff.symm !nonneg_of_int
-           ... ↔ nonneg (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
-           ... ↔ of_int a ≤ of_int b          : iff.rfl)
+  a ≤ b ↔ b - a ≥ 0                    : iff.symm !sub_nonneg_iff_le
+    ... ↔ nonneg (of_int (b - a))      : iff.symm !nonneg_of_int
+    ... ↔ nonneg (of_int b - of_int a) : !of_int_sub ▸ iff.rfl
+    ... ↔ of_int a ≤ of_int b          : iff.rfl)
 
-theorem of_int_le_of_int_of_le {a b : ℤ} (H : (#int a ≤ b)) : of_int a ≤ of_int b :=
+theorem of_int_le_of_int_of_le {a b : ℤ} (H : a ≤ b) : of_int a ≤ of_int b :=
 iff.mpr !of_int_le_of_int_iff H
 
-theorem le_of_of_int_le_of_int {a b : ℤ} (H : of_int a ≤ of_int b) : (#int a ≤ b) :=
+theorem le_of_of_int_le_of_int {a b : ℤ} (H : of_int a ≤ of_int b) : a ≤ b :=
 iff.mp !of_int_le_of_int_iff H
 
-theorem of_nat_lt_of_nat_iff (a b : ℕ) : of_nat a < of_nat b ↔ (#nat a < b) :=
+theorem of_nat_lt_of_nat_iff (a b : ℕ) : of_nat a < of_nat b ↔ a < b :=
 by rewrite [*of_nat_eq, of_int_lt_of_int_iff, int.of_nat_lt_of_nat_iff]
 
-theorem of_nat_lt_of_nat_of_lt {a b : ℕ} (H : (#nat a < b)) : of_nat a < of_nat b :=
+theorem of_nat_lt_of_nat_of_lt {a b : ℕ} (H : a < b) : of_nat a < of_nat b :=
 iff.mpr !of_nat_lt_of_nat_iff H
 
-theorem lt_of_of_nat_lt_of_nat {a b : ℕ} (H : of_nat a < of_nat b) : (#nat a < b) :=
+theorem lt_of_of_nat_lt_of_nat {a b : ℕ} (H : of_nat a < of_nat b) : a < b :=
 iff.mp !of_nat_lt_of_nat_iff H
 
-theorem of_nat_le_of_nat_iff (a b : ℕ) : of_nat a ≤ of_nat b ↔ (#nat a ≤ b) :=
+theorem of_nat_le_of_nat_iff (a b : ℕ) : of_nat a ≤ of_nat b ↔ a ≤ b :=
 by rewrite [*of_nat_eq, of_int_le_of_int_iff, int.of_nat_le_of_nat_iff]
 
-theorem of_nat_le_of_nat_of_le {a b : ℕ} (H : (#nat a ≤ b)) : of_nat a ≤ of_nat b :=
+theorem of_nat_le_of_nat_of_le {a b : ℕ} (H : a ≤ b) : of_nat a ≤ of_nat b :=
 iff.mpr !of_nat_le_of_nat_iff H
 
-theorem le_of_of_nat_le_of_nat {a b : ℕ} (H : of_nat a ≤ of_nat b) : (#nat a ≤ b) :=
+theorem le_of_of_nat_le_of_nat {a b : ℕ} (H : of_nat a ≤ of_nat b) : a ≤ b :=
 iff.mp !of_nat_le_of_nat_iff H
 
 theorem of_nat_nonneg (a : ℕ) : (of_nat a ≥ 0) :=
 of_nat_le_of_nat_of_le !nat.zero_le
 
 theorem le.refl (a : ℚ) : a ≤ a :=
-by rewrite [↑rat.le, sub_self]; apply nonneg_zero
+by rewrite [le.def, sub_self]; apply nonneg_zero
 
 theorem le.trans (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
 assert H3 : nonneg (c - b + (b - a)), from nonneg_add H2 H1,
 begin
   revert H3,
-  rewrite [↑rat.sub, add.assoc, neg_add_cancel_left],
+  krewrite [rat.sub.def, add.assoc, neg_add_cancel_left],
   intro H3, apply H3
 end
 
@@ -218,7 +221,7 @@ eq_of_sub_eq_zero H4
 theorem le.total (a b : ℚ) : a ≤ b ∨ b ≤ a :=
 or.elim (nonneg_total (b - a))
   (assume H, or.inl H)
-  (assume H, or.inr (!neg_sub ▸ H))
+  (assume H, or.inr begin rewrite neg_sub at H, exact H end)
 
 theorem le.by_cases {P : Prop} (a b : ℚ) (H : a ≤ b → P) (H2 : b ≤ a → P) : P :=
   or.elim (!rat.le.total) H H2
@@ -250,19 +253,19 @@ by intros; rewrite -sub_zero; eassumption
 
 theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b :=
 have c + b - (c + a) = b - a,
-  by rewrite [↑sub, neg_add, -add.assoc, add.comm c, add_neg_cancel_right],
+  by rewrite [sub.def, neg_add, -add.assoc, add.comm c, add_neg_cancel_right],
 show nonneg (c + b - (c + a)), from this⁻¹ ▸ H
 
 theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 : ℚ) :=
-have nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
-!sub_zero⁻¹ ▸ this
+assert nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
+begin rewrite -sub_zero at this, exact this end
 
 private theorem to_pos : a > 0 → pos a :=
 by intros; rewrite -sub_zero; eassumption
 
 theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
-have pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
-!sub_zero⁻¹ ▸ this
+assert pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
+begin rewrite -sub_zero at this, exact this end
 
 definition decidable_lt [instance] : decidable_rel rat.lt :=
 take a b, decidable_pos (b - a)
@@ -299,52 +302,25 @@ let H' := le_of_lt H in
                                   (take Heq, let Heq' := add_left_cancel Heq in
                                    !lt_irrefl (Heq' ▸ H)))
 
-section migrate_algebra
-  open [classes] algebra
-
-  protected definition discrete_linear_ordered_field [reducible] :
+protected definition discrete_linear_ordered_field [reducible] [instance] :
     algebra.discrete_linear_ordered_field rat :=
-  ⦃algebra.discrete_linear_ordered_field,
-    rat.discrete_field,
-    le_refl          := le.refl,
-    le_trans         := @le.trans,
-    le_antisymm      := @le.antisymm,
-    le_total         := @le.total,
-    le_of_lt         := @le_of_lt,
-    lt_irrefl        := lt_irrefl,
-    lt_of_lt_of_le   := @lt_of_lt_of_le,
-    lt_of_le_of_lt   := @lt_of_le_of_lt,
-    le_iff_lt_or_eq  := @le_iff_lt_or_eq,
-    add_le_add_left  := @add_le_add_left,
-    mul_nonneg       := @mul_nonneg,
-    mul_pos          := @mul_pos,
-    decidable_lt     := @decidable_lt,
-    zero_lt_one      := zero_lt_one,
-    add_lt_add_left  := @add_lt_add_left⦄
-
-  local attribute rat.discrete_linear_ordered_field [trans-instance]
-  local attribute rat.discrete_field [instance]
-
-  definition min : ℚ → ℚ → ℚ := algebra.min
-  definition max : ℚ → ℚ → ℚ := algebra.max
-  definition abs : ℚ → ℚ := algebra.abs
-  definition sign : ℚ → ℚ := algebra.sign
-
-  migrate from algebra with rat
-    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
-
-  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]
-
-  attribute decidable_le [instance]
-
-end migrate_algebra
+⦃algebra.discrete_linear_ordered_field,
+ rat.discrete_field,
+ le_refl          := le.refl,
+ le_trans         := @le.trans,
+ le_antisymm      := @le.antisymm,
+ le_total         := @le.total,
+ le_of_lt         := @le_of_lt,
+ lt_irrefl        := lt_irrefl,
+ lt_of_lt_of_le   := @lt_of_lt_of_le,
+ lt_of_le_of_lt   := @lt_of_le_of_lt,
+ le_iff_lt_or_eq  := @le_iff_lt_or_eq,
+ add_le_add_left  := @add_le_add_left,
+ mul_nonneg       := @mul_nonneg,
+ mul_pos          := @mul_pos,
+ decidable_lt     := @decidable_lt,
+ zero_lt_one      := zero_lt_one,
+ add_lt_add_left  := @add_lt_add_left⦄
 
 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,
@@ -363,10 +339,10 @@ theorem eq_zero_of_nonneg_of_forall_lt {x : ℚ} (xnonneg : x ≥ 0) (H : ∀ ε
 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,
+  take ε, suppose h₁ : ε > 0,
+  have ε / 2 > 0, from div_pos_of_pos_of_pos h₁ two_pos,
   have x ≤ ε / 2, from H _ this,
-  show x < ε, from lt_of_le_of_lt this (rat.div_two_lt_of_pos `ε > 0`),
+  show x < ε, from lt_of_le_of_lt this (div_two_lt_of_pos h₁),
 eq_zero_of_nonneg_of_forall_lt xnonneg H'
 
 theorem eq_zero_of_forall_abs_le {x : ℚ} (H : ∀ ε, ε > 0 → abs x ≤ ε) :
@@ -384,8 +360,6 @@ eq_of_sub_eq_zero this
 section
   open int
 
-  set_option pp.coercions true
-
   theorem num_nonneg_of_nonneg {q : ℚ} (H : q ≥ 0) : num q ≥ 0 :=
   have of_int (num q) ≥ of_int 0,
     begin
@@ -411,6 +385,7 @@ section
     begin
       rewrite [-mul_denom],
       apply mul_neg_of_neg_of_pos H,
+      change of_int (denom q) > of_int 0,
       rewrite [of_int_lt_of_int_iff],
       exact !denom_pos
     end,
@@ -421,6 +396,7 @@ section
     begin
       rewrite [-mul_denom],
       apply mul_nonpos_of_nonpos_of_nonneg H,
+      change of_int (denom q) ≥ of_int 0,
       rewrite [of_int_le_of_int_iff],
       exact int.le_of_lt !denom_pos
     end,
@@ -443,25 +419,27 @@ have abs a ≤ abs (of_int (num a)), from
 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
+  ... ≤ abs (of_int (num a)) + 1                : le_add_of_nonneg_right trivial
   ... = 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
+theorem ubound_pos (a : ℚ) : ubound a > 0 :=
+!nat.succ_pos
 
-theorem binary_nat_bound (a : ℕ) : of_nat a ≤ pow 2 a :=
+open nat
+
+theorem binary_nat_bound (a : ℕ) : of_nat a ≤ 2^a :=
   nat.induction_on a (zero_le_one)
-   (take n, assume Hn,
+   (take n : nat, assume Hn,
     calc
      of_nat (nat.succ n) = (of_nat n) + 1 : of_nat_add
-       ... ≤ pow 2 n + 1 : add_le_add_right Hn
-       ... ≤ pow 2 n + rat.pow 2 n :
-             add_le_add_left (pow_ge_one_of_ge_one two_ge_one _)
-       ... = pow 2 (nat.succ n) : pow_two_add)
+       ... ≤ 2^n + 1           : algebra.add_le_add_right Hn
+       ... ≤ 2^n + (2:rat)^n   : add_le_add_left (pow_ge_one_of_ge_one two_ge_one _)
+       ... = 2^(succ n)        : pow_two_add)
 
-theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ pow 2 n :=
+theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ 2^n :=
   exists.intro (ubound a) (calc
       a ≤ of_nat (ubound a) : ubound_ge
-    ... ≤ pow 2 (ubound a) : binary_nat_bound)
+    ... ≤ 2^(ubound a) : binary_nat_bound)
 
 end rat
diff --git a/library/data/stream.lean b/library/data/stream.lean
index 0091bb758..1744e5535 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -625,13 +625,13 @@ lemma stream_equiv_of_equiv {A B : Type} : A ≃ B → stream A ≃ stream B
    begin intros, rewrite [map_map, id_of_righ_inverse r, map_id] end
 end
 
-definition lex (lt : A → A → Prop) (s₁ s₂ : stream A) : Prop :=
-∃ i, lt (nth i s₁) (nth i s₂) ∧ ∀ j, j < i → nth j s₁ = nth j s₂
+definition lex (rel : A → A → Prop) (s₁ s₂ : stream A) : Prop :=
+∃ i, rel (nth i s₁) (nth i s₂) ∧ ∀ j, j < i → nth j s₁ = nth j s₂
 
-definition lex.trans {s₁ s₂ s₃} {lt : A → A → Prop} : transitive lt → lex lt s₁ s₂ → lex lt s₂ s₃ → lex lt s₁ s₃ :=
+definition lex.trans {s₁ s₂ s₃} {rel : A → A → Prop} : transitive rel → lex rel s₁ s₂ → lex rel s₂ s₃ → lex rel s₁ s₃ :=
 assume htrans h₁ h₂,
-obtain i₁ hlt₁ he₁, from h₁,
-obtain i₂ hlt₂ he₂, from h₂,
+obtain (i₁ : nat) hlt₁ he₁, from h₁,
+obtain (i₂ : nat) hlt₂ he₂, from h₂,
 lt.by_cases
   (λ i₁lti₂ : i₁ < i₂,
     assert aux : nth i₁ s₂ = nth i₁ s₃, from he₂ _ i₁lti₂,
diff --git a/library/init/nat.lean b/library/init/nat.lean
index eb9f51f32..bdd51d0e9 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -46,7 +46,7 @@ namespace nat
   protected definition is_inhabited [instance] : inhabited nat :=
   inhabited.mk zero
 
-  protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y)
+  protected definition has_decidable_eq [instance] [priority nat.prio] : ∀ x y : nat, decidable (x = y)
   | has_decidable_eq zero     zero     := inl rfl
   | has_decidable_eq (succ x) zero     := inr (by contradiction)
   | has_decidable_eq zero     (succ y) := inr (by contradiction)
@@ -70,7 +70,7 @@ namespace nat
   theorem pred_le_iff_true [simp] (n : ℕ) : pred n ≤ n ↔ true :=
   iff_true_intro (pred_le n)
 
-  theorem le.trans [trans] {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
+  theorem le.trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
   le.rec H1 (λp H2, le.step)
 
   theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.trans H !le_succ
@@ -117,13 +117,13 @@ namespace nat
   theorem zero_lt_succ_iff_true [simp] (n : ℕ) : 0 < succ n ↔ true :=
   iff_true_intro (zero_lt_succ n)
 
-  theorem lt.trans [trans] {n m k : ℕ} (H1 : n < m) : m < k → n < k :=
+  theorem lt.trans {n m k : ℕ} (H1 : n < m) : m < k → n < k :=
   le.trans (le.step H1)
 
-  theorem lt_of_le_of_lt [trans] {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k :=
+  theorem lt_of_le_of_lt {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k :=
   le.trans (succ_le_succ H1)
 
-  theorem lt_of_lt_of_le [trans] {n m k : ℕ} : n < m → m ≤ k → n < k := le.trans
+  theorem lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := le.trans
 
   theorem lt.irrefl (n : ℕ) : ¬n < n := not_succ_le_self
 
@@ -183,13 +183,13 @@ namespace nat
   theorem lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b :=
   le_of_succ_le_succ
 
-  definition decidable_le [instance] : ∀ a b : nat, decidable (a ≤ b)  :=
+  definition decidable_le [instance] [priority nat.prio] : ∀ a b : nat, decidable (a ≤ b)  :=
   nat.rec (λm, (decidable.inl !zero_le))
      (λn IH m, !nat.cases_on (decidable.inr (not_succ_le_zero n))
        (λm, decidable.rec (λH, inl (succ_le_succ H))
           (λH, inr (λa, H (le_of_succ_le_succ a))) (IH m)))
 
-  definition decidable_lt [instance] : ∀ a b : nat, decidable (a < b) :=
+  definition decidable_lt [instance] [priority nat.prio] : ∀ a b : nat, decidable (a < b) :=
   λ a b, decidable_le (succ a) b
 
   theorem lt_or_ge (a b : ℕ) : a < b ∨ a ≥ b :=
diff --git a/library/theories/combinatorics/choose.lean b/library/theories/combinatorics/choose.lean
index 1458d0cc4..156b03d5a 100644
--- a/library/theories/combinatorics/choose.lean
+++ b/library/theories/combinatorics/choose.lean
@@ -7,6 +7,7 @@ Binomial coefficients, "n choose k".
 -/
 import data.nat.div data.nat.fact data.finset
 open decidable
+open - [notations] algebra
 
 namespace nat
 
diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean
index 1d941d018..2c9689973 100644
--- a/library/theories/number_theory/bezout.lean
+++ b/library/theories/number_theory/bezout.lean
@@ -13,6 +13,7 @@ section Bezout
 
 open nat int
 open eq.ops well_founded decidable prod
+open - [notations] algebra
 
 private definition pair_nat.lt : ℕ × ℕ → ℕ × ℕ → Prop := measure pr₂
 private definition pair_nat.lt.wf : well_founded pair_nat.lt := intro_k (measure.wf pr₂) 20
@@ -40,23 +41,36 @@ theorem egcd_succ (x y : ℕ) :
   egcd x (succ y) = prod.cases_on (egcd (succ y) (x mod succ y)) (egcd_rec_f (x div succ y)) :=
 well_founded.fix_eq egcd.F (x, succ y)
 
+set_option pp.coercions true
+
 theorem egcd_of_pos (x : ℕ) {y : ℕ} (ypos : y > 0) :
   let erec := egcd y (x mod y), u := pr₁ erec, v := pr₂ erec in
     egcd x y = (v, u - v * (x div y)) :=
-obtain y' (yeq : y = succ y'), from exists_eq_succ_of_pos ypos,
-by rewrite [yeq, egcd_succ, -prod.eta (egcd _ _)]
+obtain (y' : nat) (yeq : y = succ y'), from exists_eq_succ_of_pos ypos,
+begin
+  rewrite [yeq, egcd_succ, -prod.eta (egcd _ _)],
+  esimp, unfold egcd_rec_f,
+  rewrite [of_nat_div]
+end
 
 theorem egcd_prop (x y : ℕ) : (pr₁ (egcd x y)) * x + (pr₂ (egcd x y)) * y = gcd x y :=
 gcd.induction x y
-  (take m, by rewrite [egcd_zero, ▸*, int.mul_zero, int.one_mul])
+  (take m, by krewrite [egcd_zero, algebra.mul_zero, algebra.one_mul])
   (take m n,
     assume npos : 0 < n,
     assume IH,
     begin
       let H := egcd_of_pos m npos, esimp at H,
-      rewrite [H, ▸*, gcd_rec, -IH, add.comm (#int _ * _), -of_nat_mod, ↑modulo],
-      rewrite [*int.mul_sub_right_distrib, *int.mul_sub_left_distrib, *mul.left_distrib],
-      rewrite [sub_add_eq_add_sub, *sub_eq_add_neg, int.add.assoc, of_nat_div, *int.mul.assoc]
+      rewrite H,
+      esimp,
+      rewrite [gcd_rec, -IH],
+      rewrite [algebra.add.comm],
+      rewrite [-of_nat_mod],
+      rewrite [int.modulo.def],
+      rewrite [+algebra.mul_sub_right_distrib],
+      rewrite [+algebra.mul_sub_left_distrib, *mul.left_distrib],
+      rewrite [*sub_eq_add_neg, {pr₂ (egcd n (m mod n)) * of_nat m + - _}algebra.add.comm, -algebra.add.assoc],
+      rewrite [algebra.mul.assoc]
     end)
 
 theorem Bezout_aux (x y : ℕ) : ∃ a b : ℤ, a * x + b * y = gcd x y :=
@@ -79,25 +93,26 @@ implies prime (dvd_or_dvd_of_prime_of_dvd_mul).
 
 namespace nat
 open int
+open - [notations] algebra
 
 example {p x y : ℕ} (pp : prime p) (H : p ∣ x * y) : p ∣ x ∨ p ∣ y :=
 decidable.by_cases
   (suppose p ∣ x, or.inl this)
   (suppose ¬ p ∣ x,
     have cpx : coprime p x, from coprime_of_prime_of_not_dvd pp this,
-    obtain (a b : ℤ) (Hab : a * p + b * x = gcd p x), from !Bezout_aux,
+    obtain (a b : ℤ) (Hab : a * p + b * x = gcd p x), from Bezout_aux p x,
     assert a * p * y + b * x * y = y,
       by rewrite [-int.mul.right_distrib, Hab, ↑coprime at cpx, cpx, int.one_mul],
     have p ∣ y,
       begin
         apply dvd_of_of_nat_dvd_of_nat,
         rewrite [-this],
-        apply int.dvd_add,
-          {apply int.dvd_mul_of_dvd_left,
-            apply int.dvd_mul_of_dvd_right,
-            apply int.dvd.refl},
+        apply @dvd_add,
+          {apply dvd_mul_of_dvd_left,
+            apply dvd_mul_of_dvd_right,
+            apply dvd.refl},
           {rewrite int.mul.assoc,
-            apply int.dvd_mul_of_dvd_right,
+            apply dvd_mul_of_dvd_right,
             apply of_nat_dvd_of_nat_of_dvd H}
       end,
     or.inr this)
diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean
index 82c9fa7b6..fe7698bf5 100644
--- a/library/theories/number_theory/prime_factorization.lean
+++ b/library/theories/number_theory/prime_factorization.lean
@@ -11,6 +11,7 @@ Multiplicity and prime factors. We have:
 -/
 import data.nat data.finset .primes
 open eq.ops finset well_founded decidable nat.finset
+open - [notations] algebra
 
 namespace nat
 
@@ -119,7 +120,7 @@ private theorem mult_pow_mul {p n : ℕ} (i : ℕ) (pgt1 : p > 1) (npos : n > 0)
   mult p (p^i * n) = i + mult p n :=
 begin
   induction i with [i, ih],
-    {rewrite [pow_zero, one_mul, zero_add]},
+    {krewrite [pow_zero, one_mul, zero_add]},
   have p > 0, from lt.trans zero_lt_one pgt1,
   have psin_pos : p^(succ i) * n > 0, from mul_pos (!pow_pos_of_pos this) npos,
   have p ∣ p^(succ i) * n, by rewrite [pow_succ, mul.assoc]; apply dvd_mul_right,
@@ -128,7 +129,7 @@ begin
 end
 
 theorem mult_pow_self {p : ℕ} (i : ℕ) (pgt1 : p > 1) : mult p (p^i) = i :=
-by rewrite [-(mul_one (p^i)), mult_pow_mul i pgt1 zero_lt_one, mult_one_right]
+by krewrite [-(mul_one (p^i)), mult_pow_mul i pgt1 zero_lt_one, mult_one_right]
 
 theorem mult_self {p : ℕ} (pgt1 : p > 1) : mult p p = 1 :=
 by rewrite [-pow_one p at {2}]; apply mult_pow_self 1 pgt1
@@ -174,7 +175,7 @@ calc
 theorem mult_pow {p m : ℕ} (n : ℕ) (mpos : m > 0) (primep : prime p) : mult p (m^n) = n * mult p m :=
 begin
   induction n with n ih,
-    rewrite [pow_zero, mult_one_right, zero_mul],
+    krewrite [pow_zero, mult_one_right, zero_mul],
   rewrite [pow_succ, mult_mul primep mpos (!pow_pos_of_pos mpos), ih, succ_mul, add.comm]
 end
 
@@ -246,7 +247,7 @@ theorem mult_pow_eq_zero_of_prime_of_ne {p q : ℕ} (primep : prime p) (primeq :
   (pneq : p ≠ q) (i : ℕ) : mult p (q^i) = 0 :=
 begin
   induction i with i ih,
-    {rewrite [pow_zero, mult_one_right]},
+    {krewrite [pow_zero, mult_one_right]},
   have qpos : q > 0, from pos_of_prime primeq,
   have qipos : q^i > 0, from !pow_pos_of_pos qpos,
   rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep primeq pneq]