From bddc84664cadb5df2b66a62e7af75c2d0cdc9789 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 Feb 2018 09:53:50 -0800
Subject: [PATCH] chore(library/init/data/nat): remove pow.lean

---
 library/init/data/nat/basic.lean   | 12 ++++++++++++
 library/init/data/nat/default.lean |  2 +-
 library/init/data/nat/lemmas.lean  |  4 +++-
 library/init/data/nat/pow.lean     | 26 --------------------------
 4 files changed, 16 insertions(+), 28 deletions(-)
 delete mode 100644 library/init/data/nat/pow.lean

diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index bdfb04674c..2bc927a867 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -195,4 +195,16 @@ protected lemma bit1_ne_zero (n : ℕ) : bit1 n ≠ 0 :=
 show succ (n + n) ≠ 0, from
 λ h, nat.no_confusion h
 
+/- Exponentiation -/
+
+def pow (b : ℕ) : ℕ → ℕ
+| 0        := 1
+| (succ n) := pow n * b
+
+infix `^` := pow
+
+lemma pow_succ (b n : ℕ) : b^(succ n) = b^n * b := rfl
+
+@[simp] lemma pow_zero (b : ℕ) : b^0 = 1 := rfl
+
 end nat
diff --git a/library/init/data/nat/default.lean b/library/init/data/nat/default.lean
index 148404126c..00050a9423 100644
--- a/library/init/data/nat/default.lean
+++ b/library/init/data/nat/default.lean
@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.nat.basic init.data.nat.div init.data.nat.pow init.data.nat.lemmas
+import init.data.nat.basic init.data.nat.div init.data.nat.lemmas
        init.data.nat.bitwise
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index c0cc7812d5..c78d83eec0 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
-import init.data.nat.basic init.data.nat.div init.data.nat.pow init.meta init.algebra.functions
+import init.data.nat.basic init.data.nat.div init.meta init.algebra.functions
 universes u
 
 namespace nat
@@ -1350,4 +1350,6 @@ begin
       simp [h₁] },
     rw [eq.symm (mod_eq_sub_mod p_b_ge)] }
 end
+
+
 end nat
diff --git a/library/init/data/nat/pow.lean b/library/init/data/nat/pow.lean
deleted file mode 100644
index 2f049b1af7..0000000000
--- a/library/init/data/nat/pow.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-/-
-Copyright (c) 2017 Galois Inc. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Simon Hudon
-
-exponentiation on natural numbers
-
-This is a work-in-progress
--/
-prelude
-
-import init.data.nat.basic init.meta
-
-namespace nat
-
-def pow (b : ℕ) : ℕ → ℕ
-| 0        := 1
-| (succ n) := pow n * b
-
-infix `^` := pow
-
-lemma pow_succ (b n : ℕ) : b^(succ n) = b^n * b := rfl
-
-@[simp] lemma pow_zero (b : ℕ) : b^0 = 1 := rfl
-
-end nat