diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean
index 291953e97..dde566b5c 100644
--- a/library/algebra/group_bigops.lean
+++ b/library/algebra/group_bigops.lean
@@ -84,7 +84,7 @@ section monoid
   | (a::l) := take b, assume Pconst,
     assert Pconstl : ∀ a', a' ∈ l → f a' = b,
       from take a' Pa'in, Pconst a' (mem_cons_of_mem a Pa'in),
-    by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons, add_one, pow_succ' b]
+    by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons, add_one, pow_succ b]
 
 end monoid
 
diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean
index 6ce85c884..e8c5f1969 100644
--- a/library/algebra/group_power.lean
+++ b/library/algebra/group_power.lean
@@ -26,30 +26,45 @@ include s
 
 definition pow (a : A) : ℕ → A
 | 0     := 1
-| (n+1) := pow n * a
+| (n+1) := a * pow n
 
 infix [priority algebra.prio] `^` := pow
 
 theorem pow_zero (a : A) : a^0 = 1 := rfl
-theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a^n * a := rfl
+theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a * a^n := rfl
 
-theorem pow_succ' (a : A) : ∀n, a^(succ n) = a * a^n
+theorem pow_one (a : A) : a^1 = a := !mul_one
+theorem pow_two (a : A) : a^2 = a * a :=
+calc
+  a^2 = a * (a * 1) : rfl
+  ... = a * a       : mul_one
+theorem pow_three (a : A) : a^3 = a * (a * a) :=
+calc
+  a^3 = a * (a * (a * 1)) : rfl
+  ... = a * (a * a)       : mul_one
+theorem pow_four (a : A) : a^4 = a * (a * (a * a))  :=
+calc
+  a^4 = a * a^3           : rfl
+  ... = a * (a * (a * a)) : pow_three
+
+theorem pow_succ' (a : A) : ∀n, a^(succ n) = a^n * a
 | 0        := by rewrite [pow_succ, *pow_zero, one_mul, mul_one]
 | (succ n) := by rewrite [pow_succ, pow_succ' at {1}, pow_succ, mul.assoc]
 
 theorem one_pow : ∀ n : ℕ, 1^n = (1:A)
 | 0        := rfl
-| (succ n) := by rewrite [pow_succ, mul_one, one_pow]
+| (succ n) := by rewrite [pow_succ, one_mul, one_pow]
 
-theorem pow_one (a : A) : a^1 = a := !one_mul
-
-theorem pow_add (a : A) (m : ℕ) : ∀ n, a^(m + n) = a^m * a^n
-| 0        := by rewrite [nat.add_zero, pow_zero, mul_one]
-| (succ n) := by rewrite [add_succ, *pow_succ, pow_add, mul.assoc]
+theorem pow_add (a : A) (m n : ℕ) : a^(m + n) = a^m * a^n :=
+begin
+  induction n with n ih,
+    {rewrite [nat.add_zero, pow_zero, mul_one]},
+  rewrite [add_succ, *pow_succ', ih, mul.assoc]
+end
 
 theorem pow_mul (a : A) (m : ℕ) : ∀ n, a^(m * n) = (a^m)^n
 | 0        := by rewrite [nat.mul_zero, pow_zero]
-| (succ n) := by rewrite [nat.mul_succ, pow_add, pow_succ, pow_mul]
+| (succ n) := by rewrite [nat.mul_succ, pow_add, pow_succ', pow_mul]
 
 theorem pow_comm (a : A) (m n : ℕ)  : a^m * a^n = a^n * a^m :=
 by rewrite [-*pow_add, nat.add.comm]
@@ -65,7 +80,7 @@ include s
 
 theorem mul_pow (a b : A) : ∀ n, (a * b)^n = a^n * b^n
 | 0        := by rewrite [*pow_zero, mul_one]
-| (succ n) := by rewrite [*pow_succ, mul_pow, *mul.assoc, mul.left_comm a]
+| (succ n) := by rewrite [*pow_succ', mul_pow, *mul.assoc, mul.left_comm a]
 
 end comm_monoid
 
@@ -87,7 +102,7 @@ eq_mul_inv_of_mul_eq H2
 theorem pow_inv_comm (a : A) : ∀m n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m
 | 0 n               := by rewrite [*pow_zero, one_mul, mul_one]
 | m 0               := by rewrite [*pow_zero, one_mul, mul_one]
-| (succ m) (succ n) := by rewrite [pow_succ at {1}, pow_succ' at {1}, pow_succ, pow_succ',
+| (succ m) (succ n) := by rewrite [pow_succ' at {1}, pow_succ at {1}, pow_succ', pow_succ,
                             *mul.assoc, inv_mul_cancel_left, mul_inv_cancel_left, pow_inv_comm]
 
 end nat
@@ -143,7 +158,7 @@ theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : pow a n > 0 :=
     induction n,
     rewrite pow_zero,
     apply zero_lt_one,
-    rewrite pow_succ,
+    rewrite pow_succ',
     apply mul_pos,
     apply v_0, apply H
   end
@@ -153,7 +168,7 @@ theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : pow a n ≥ 1 :=
     induction n,
     rewrite pow_zero,
     apply le.refl,
-    rewrite [pow_succ, -{1}mul_one],
+    rewrite [pow_succ', -{1}mul_one],
     apply mul_le_mul v_0 H zero_le_one,
     apply le_of_lt,
     apply pow_pos,
@@ -163,7 +178,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) :=
-  by rewrite [pow_succ, left_distrib, *mul_one]
+  by rewrite [pow_succ', left_distrib, *mul_one]
 
 end ordered_ring
 
@@ -180,9 +195,9 @@ definition nmul : ℕ → A → A := λ n a, pow a n
 infix [priority algebra.prio] `⬝` := nmul
 
 theorem zero_nmul (a : A) : (0:ℕ) ⬝ a = 0 := pow_zero a
-theorem succ_nmul (n : ℕ) (a : A) : succ n ⬝ a = nmul n a + a := pow_succ a n
+theorem succ_nmul (n : ℕ) (a : A) : nmul (succ n) a = a + (nmul n a) := pow_succ a n
 
-theorem succ_nmul' (n : ℕ) (a : A) : nmul (succ n) a = a + (nmul n a) := pow_succ' a n
+theorem succ_nmul' (n : ℕ) (a : A) : succ n ⬝ a = nmul n a + a := pow_succ' a n
 
 theorem nmul_zero (n : ℕ) : n ⬝ 0 = (0:A) := one_pow n
 
diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean
index f062cc477..9a0a49df2 100644
--- a/library/algebra/ring_power.lean
+++ b/library/algebra/ring_power.lean
@@ -22,14 +22,14 @@ theorem pow_pos_of_pos {x : A} (i : ℕ) (H : x > 0) : x^i > 0 :=
 begin
   induction i with [j, ih],
     {show (1 : A) > 0, from zero_lt_one},
-    {show x^(succ j) > 0, from mul_pos ih H}
+    {show x^(succ j) > 0, from mul_pos H ih}
 end
 
 theorem pow_nonneg_of_nonneg {x : A} (i : ℕ) (H : x ≥ 0) : x^i ≥ 0 :=
 begin
   induction i with [j, ih],
     {show (1 : A) ≥ 0, from le_of_lt zero_lt_one},
-    {show x^(succ j) ≥ 0, from mul_nonneg ih H}
+    {show x^(succ j) ≥ 0, from mul_nonneg H ih}
 end
 
 theorem pow_le_pow_of_le {x y : A} (i : ℕ) (H₁ : 0 ≤ x) (H₂ : x ≤ y) : x^i ≤ y^i :=
@@ -37,8 +37,8 @@ begin
   induction i with [i, ih],
     {rewrite *pow_zero, apply le.refl},
   rewrite *pow_succ,
-  have H : 0 ≤ y^i, from pow_nonneg_of_nonneg i (le.trans H₁ H₂),
-  apply mul_le_mul ih H₂ H₁ H
+  have H : 0 ≤ x^i, from pow_nonneg_of_nonneg i H₁,
+  apply mul_le_mul H₂ ih H (le.trans H₁ H₂)
 end
 
 theorem pow_ge_one {x : A} (i : ℕ) (xge1 : x ≥ 1) : x^i ≥ 1 :=
@@ -53,7 +53,7 @@ begin
   induction i with [i, ih],
     {exfalso, exact !nat.lt.irrefl ipos},
   have xige1 : x^i ≥ 1, from pow_ge_one _ (le_of_lt xgt1),
-  rewrite [pow_succ', -mul_one 1, ↑has_lt.gt],
+  rewrite [pow_succ, -mul_one 1, ↑has_lt.gt],
   apply mul_lt_mul xgt1 xige1 zero_lt_one,
   apply le_of_lt xpos
 end
diff --git a/library/data/finset/equiv.lean b/library/data/finset/equiv.lean
index 0dda8e76a..0b1b95066 100644
--- a/library/data/finset/equiv.lean
+++ b/library/data/finset/equiv.lean
@@ -48,11 +48,11 @@ private lemma succ_mem_of_nat (n : nat) (s : nat) : succ n ∈ of_nat s ↔ n 
 iff.intro
   (suppose succ n ∈ of_nat s,
    assert odd (s div 2^(succ n)),    from odd_of_mem_of_nat this,
-   have odd ((s div 2) div (2 ^ n)), by rewrite [pow_succ at this, div_div_eq_div_mul, mul.comm]; assumption,
+   have odd ((s div 2) div (2 ^ n)), by rewrite [pow_succ' at this, div_div_eq_div_mul, mul.comm]; assumption,
    show n ∈ of_nat (s div 2),        from mem_of_nat_of_odd this)
   (suppose n ∈ of_nat (s div 2),
    assert odd ((s div 2) div (2 ^ n)), from odd_of_mem_of_nat this,
-   assert odd (s div 2^(succ n)),      by rewrite [pow_succ, mul.comm, -div_div_eq_div_mul]; assumption,
+   assert odd (s div 2^(succ n)),      by rewrite [pow_succ', mul.comm, -div_div_eq_div_mul]; assumption,
    show succ n ∈ of_nat s,             from mem_of_nat_of_odd this)
 
 private lemma odd_of_zero_mem (s : nat) : 0 ∈ of_nat s ↔ odd s :=
@@ -93,7 +93,7 @@ finset.induction_on s dec_trivial
                 assert a ≠ 0, from suppose a = 0, by subst a; contradiction,
                 begin
                   cases a with a, contradiction,
-                  have odd (2*2^a),  by rewrite [pow_succ at o, mul.comm]; exact o,
+                  have odd (2*2^a),  by rewrite [pow_succ' at o, mul.comm]; exact o,
                   have even (2*2^a), from !even_two_mul,
                   exact absurd `even (2*2^a)` `odd (2*2^a)`
                 end))),
@@ -104,7 +104,7 @@ finset.induction_on s dec_trivial
           match a with
           | 0         := suppose a = 0, absurd this `a ≠ 0`
           | (succ a') := suppose a = succ a',
-            have even (2^(succ a')), by rewrite [pow_succ, mul.comm]; apply even_two_mul,
+            have even (2^(succ a')), by rewrite [pow_succ', mul.comm]; apply even_two_mul,
             even_add_of_even_of_even this `even (to_nat s)`
           end rfl
     end)
@@ -144,7 +144,7 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n
   finset.ext (λ x,
   have gen : ∀ m, m ∈ of_nat (2^(succ n) + s) ↔ m ∈ insert (succ n) (of_nat s)
   | zero     :=
-    have even (2^(succ n)), by rewrite [pow_succ, mul.comm]; apply even_two_mul,
+    have even (2^(succ n)), by rewrite [pow_succ', mul.comm]; apply even_two_mul,
     have aux₁ : odd (2^(succ n) + s) ↔ odd s, from iff.intro
       (suppose odd (2^(succ n) + s), by_contradiction
         (suppose ¬ odd s,
@@ -172,7 +172,7 @@ private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n
          by subst m; apply mem_insert)
         (suppose succ m ∈ of_nat s, finset.mem_insert_of_mem _ (iff.mp !succ_mem_of_nat this))),
     calc
-      succ m ∈ of_nat (2^(succ n) + s) ↔ succ m ∈ of_nat (2^n * 2 + s)       : by rewrite pow_succ
+      succ m ∈ of_nat (2^(succ n) + s) ↔ succ m ∈ of_nat (2^n * 2 + s)       : by rewrite pow_succ'
                                  ...   ↔ m ∈ of_nat ((2^n * 2 + s) div 2)    : succ_mem_of_nat
                                  ...   ↔ m ∈ of_nat (2^n + s div 2)          : by rewrite [add.comm, add_mul_div_self (dec_trivial : 2 > 0), add.comm]
                                  ...   ↔ m ∈ insert n (of_nat (s div 2))     : by rewrite ih
@@ -258,7 +258,7 @@ begin
                   mul_div_cancel _ (dec_trivial : 2 > 0), d₁, zero_add]
      end },
    { have a ∉ predimage s, from suppose a ∈ predimage s, absurd (succ_mem_of_mem_predimage this) nains,
-     rewrite [predimage_insert_succ, to_nat_insert nains, pow_succ, add.comm,
+     rewrite [predimage_insert_succ, to_nat_insert nains, pow_succ', add.comm,
               add_mul_div_self (dec_trivial : 2 > 0), -ih, to_nat_insert this, add.comm] }
 end
 
diff --git a/library/data/fintype/function.lean b/library/data/fintype/function.lean
index d8a7af2ae..5484a6276 100644
--- a/library/data/fintype/function.lean
+++ b/library/data/fintype/function.lean
@@ -94,7 +94,7 @@ lemma length_all_lists : ∀ {n : nat}, length (@all_lists_of_len A _ n) = (card
 | (succ n)  := calc length _ = card A * length (all_lists_of_len n) : length_cons_all
                          ... = card A * (card A ^ n) : length_all_lists
                          ... = (card A ^ n) * card A : nat.mul.comm
-                         ... = (card A) ^ (succ n) : pow_succ
+                         ... = (card A) ^ (succ n) : pow_succ'
 
 
 end list_of_lists
diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean
index 8c6cf7899..5487455a7 100644
--- a/library/data/nat/power.lean
+++ b/library/data/nat/power.lean
@@ -42,58 +42,58 @@ theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i
                    ... = x^j * (1 + 1) : by rewrite [mul.left_distrib, *mul_one]
                    ... = x^j * 2       : rfl
                    ... ≤ x^j * x       : mul_le_mul_left _ `x ≥ 2`
-                   ... = x^(succ j)    : rfl
+                   ... = x^(succ j)    : pow_succ'
 
 -- TODO: eventually this will be subsumed under the algebraic theorems
 
 theorem mul_self_eq_pow_2 (a : nat) : a * a = pow a 2 :=
 show a * a = pow a (succ (succ zero)), from
-by rewrite [*pow_succ, *pow_zero, one_mul]
+by rewrite [*pow_succ, *pow_zero, mul_one]
 
 theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → pow a b = pow a c → b = c
 | a 0        0        h₁ h₂ := rfl
 | a (succ b) 0        h₁ h₂ :=
-  assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
+  assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
   assert 1 < 1, by rewrite [this at h₁]; exact h₁,
   absurd `1 < 1` !lt.irrefl
 | a 0        (succ c) h₁ h₂ :=
-  assert a = 1, by rewrite [pow_succ' at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
+  assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
   assert 1 < 1, by rewrite [this at h₁]; exact h₁,
   absurd `1 < 1` !lt.irrefl
 | a (succ b) (succ c) h₁ h₂ :=
   assert a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),
-  assert pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂),
+  assert pow a b = pow a c, by rewrite [*pow_succ at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero this) h₂),
   by rewrite [pow_cancel_left h₁ this]
 
 theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → pow a (succ b) div a = pow a b
-| a 0        h := by rewrite [pow_succ', pow_zero, mul_one, div_self (pos_of_ne_zero h)]
-| a (succ b) h := by rewrite [pow_succ', mul_div_cancel_left _ (pos_of_ne_zero h)]
+| a 0        h := by rewrite [pow_succ, pow_zero, mul_one, div_self (pos_of_ne_zero h)]
+| a (succ b) h := by rewrite [pow_succ, mul_div_cancel_left _ (pos_of_ne_zero h)]
 
 lemma dvd_pow : ∀ (i : nat) {n : nat}, n > 0 → i ∣ i^n
 | i 0        h := absurd h !lt.irrefl
-| i (succ n) h := by rewrite [pow_succ]; apply dvd_mul_left
+| i (succ n) h := by rewrite [pow_succ']; apply dvd_mul_left
 
 lemma dvd_pow_of_dvd_of_pos : ∀ {i j n : nat}, i ∣ j → n > 0 → i ∣ j^n
 | i j 0        h₁ h₂ := absurd h₂ !lt.irrefl
-| i j (succ n) h₁ h₂ := by rewrite [pow_succ]; apply dvd_mul_of_dvd_right h₁
+| i j (succ n) h₁ h₂ := by rewrite [pow_succ']; apply dvd_mul_of_dvd_right h₁
 
 lemma pow_mod_eq_zero (i : nat) {n : nat} (h : n > 0) : (i^n) mod i = 0 :=
 iff.mp !dvd_iff_mod_eq_zero (dvd_pow i h)
 
 lemma pow_dvd_of_pow_succ_dvd {p i n : nat} : p^(succ i) ∣ n → p^i ∣ n :=
 suppose p^(succ i) ∣ n,
-assert p^i ∣ p^(succ i), from by rewrite [pow_succ]; apply dvd_of_eq_mul; apply rfl,
+assert p^i ∣ p^(succ i), from by rewrite [pow_succ']; apply dvd_of_eq_mul; apply rfl,
 dvd.trans `p^i ∣ p^(succ i)` `p^(succ i) ∣ n`
 
 lemma dvd_of_pow_succ_dvd_mul_pow {p i n : nat} (Ppos : p > 0) :
   p^(succ i) ∣ (n * p^i) → p ∣ n :=
-by rewrite [pow_succ']; apply dvd_of_mul_dvd_mul_right; apply pow_pos_of_pos _ Ppos
+by rewrite [pow_succ]; apply dvd_of_mul_dvd_mul_right; apply pow_pos_of_pos _ Ppos
 
 lemma coprime_pow_right {a b} : ∀ n, coprime b a → coprime b (a^n)
 | 0        h := !comprime_one_right
 | (succ n) h :=
   begin
-    rewrite [pow_succ],
+    rewrite [pow_succ'],
     apply coprime_mul_right,
       exact coprime_pow_right n h,
       exact h
diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean
index 5e26742ec..6b80cc44c 100644
--- a/library/theories/group_theory/cyclic.lean
+++ b/library/theories/group_theory/cyclic.lean
@@ -140,7 +140,7 @@ mem_sep_of_mem !mem_univ
 lemma mem_cyc (a : A) : ∀ {n : nat}, a^n ∈ cyc a
 | 0        := cyc_has_one a
 | (succ n) :=
-  begin rewrite pow_succ, apply cyc_mul_closed a, exact mem_cyc, apply self_mem_cyc end
+  begin rewrite pow_succ', apply cyc_mul_closed a, exact mem_cyc, apply self_mem_cyc end
 
 lemma order_le {a : A} {n : nat} : a^(succ n) = 1 → order a ≤ succ n :=
 assume Pe, let s := image (pow a) (upto (succ n)) in
@@ -243,7 +243,7 @@ local infix ^ := algebra.pow
 lemma pow_eq_mul {n : nat} {i : fin (succ n)} : ∀ {k : nat}, i^k = mk_mod n (i*k)
 | 0        := by rewrite [pow_zero]
 | (succ k) := begin
-  assert Psucc : i^(succ k) = madd (i^k) i, apply pow_succ,
+  assert Psucc : i^(succ k) = madd (i^k) i, apply pow_succ',
   rewrite [Psucc, pow_eq_mul],
   apply eq_of_veq,
   rewrite [mul_succ, val_madd, ↑mk_mod, mod_add_mod]
@@ -368,7 +368,7 @@ eq_of_feq (funext take f, calc
 
 lemma rotl_perm_pow_eq : ∀ {i : nat}, (rotl_perm A n 1) ^ i = rotl_perm A n i
 | 0        := begin rewrite [pow_zero, ↑rotl_perm, perm_one, -eq_iff_feq], esimp, rewrite rotl_seq_zero  end
-| (succ i) := begin rewrite [pow_succ, rotl_perm_pow_eq, rotl_perm_mul, one_add] end
+| (succ i) := begin rewrite [pow_succ', rotl_perm_pow_eq, rotl_perm_mul, one_add] end
 
 lemma rotl_perm_pow_eq_one : (rotl_perm A n 1) ^ n = 1 :=
 eq.trans rotl_perm_pow_eq (eq_of_feq begin esimp [rotl_perm], rewrite [↑rotl_fun, rotl_id] end)
diff --git a/library/theories/group_theory/pgroup.lean b/library/theories/group_theory/pgroup.lean
index 5389ec245..0c349b35f 100644
--- a/library/theories/group_theory/pgroup.lean
+++ b/library/theories/group_theory/pgroup.lean
@@ -384,7 +384,7 @@ theorem first_sylow_theorem {p : nat} (Pp : prime p) :
   obtain J PJ, from cauchy_theorem Pp Ppdvd,
   exists.intro (fin_coset_Union (cyc J))
     (exists.intro _
-      (by rewrite [pow_succ', -PcardH, -PJ]; apply card_Union_lcosets))
+      (by rewrite [pow_succ, -PcardH, -PJ]; apply card_Union_lcosets))
 
 end sylow
 
diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean
index fbb053c7f..9b8efd4a6 100644
--- a/library/theories/number_theory/prime_factorization.lean
+++ b/library/theories/number_theory/prime_factorization.lean
@@ -98,7 +98,7 @@ begin
       assert n' < n,
         by rewrite -this; apply mult_rec_decreasing pgt1 npos,
       begin
-        rewrite [mult_rec pgt1 npos pdvdn, `n div p = n'`, pow_succ'], subst n,
+        rewrite [mult_rec pgt1 npos pdvdn, `n div p = n'`, pow_succ], subst n,
         apply mul_dvd_mul !dvd.refl,
         apply ih _ this
       end)
@@ -122,8 +122,8 @@ begin
     {rewrite [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,
-  rewrite [mult_rec pgt1 psin_pos this, pow_succ, mul.right_comm, !mul_div_cancel `p > 0`, ih],
+  have p ∣ p^(succ i) * n, by rewrite [pow_succ, mul.assoc]; apply dvd_mul_right,
+  rewrite [mult_rec pgt1 psin_pos this, pow_succ', mul.right_comm, !mul_div_cancel `p > 0`, ih],
   rewrite [add.comm i, add.comm (succ i)]
 end
 
@@ -143,7 +143,7 @@ obtain m (H : n div p^(mult p n) = p * m), from exists_eq_mul_right_of_dvd pdvd,
 assert n = p^(succ (mult p n)) * m, from
   calc
     n     = p^mult p n * (n div p^mult p n) : by rewrite (mul_div_cancel' !pow_mult_dvd)
-      ... = p^(succ (mult p n)) * m         : by rewrite [H, pow_succ, mul.assoc],
+      ... = p^(succ (mult p n)) * m         : by rewrite [H, pow_succ', mul.assoc],
 have p^(succ (mult p n)) ∣ n,    by rewrite this at {2}; apply dvd_mul_right,
 have succ (mult p n) ≤ mult p n, from le_mult pgt1 npos this,
 show false,                      from !not_succ_le_self this
@@ -239,7 +239,7 @@ begin
     {rewrite [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]
+  rewrite [pow_succ', mult_mul primep qipos qpos, ih, mult_eq_zero_of_prime_of_ne primep primeq pneq]
 end
 
 theorem mult_prod_pow_of_not_mem {p : ℕ} (primep : prime p) {s : finset ℕ}
diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean
index 67def367f..c77a46237 100644
--- a/library/theories/number_theory/primes.lean
+++ b/library/theories/number_theory/primes.lean
@@ -194,7 +194,7 @@ lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p
   have   1 ≥ 2, by rewrite -this; apply ge_two_of_prime hp,
   absurd this dec_trivial
 | (succ n) hp hd :=
-  have p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd,
+  have p ∣ (m^n)*m, by rewrite [pow_succ' at hd]; exact hd,
   or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp this)
     (suppose p ∣ m^n, dvd_of_prime_of_dvd_pow hp this)
     (suppose p ∣ m, this)
@@ -226,7 +226,7 @@ lemma eq_one_or_dvd_of_dvd_prime_pow {p : nat} : ∀ {m i : nat}, prime p → i
 | 0        := take i, assume Pp, begin rewrite [pow_zero], intro Pdvd, apply or.inl (eq_one_of_dvd_one Pdvd) end
 | (succ m) := take i, assume Pp, or.elim (coprime_or_dvd_of_prime Pp i)
   (λ Pcp, begin
-    rewrite [pow_succ], intro Pdvd,
+    rewrite [pow_succ'], intro Pdvd,
     apply eq_one_or_dvd_of_dvd_prime_pow Pp,
     apply dvd_of_coprime_of_dvd_mul_right,
       apply coprime_swap Pcp, exact Pdvd