diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 9afb91f72e..eea1177aed 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -10,10 +10,6 @@ open eq.ops binary
 
 namespace nat
 
-definition of_num [coercion] [reducible] (n : num) : ℕ :=
-num.rec zero
-  (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
-
 definition addl (x y : ℕ) : ℕ :=
 nat.rec y (λ n r, succ r) x
 infix `⊕`:65 := addl
diff --git a/library/init/nat.lean b/library/init/nat.lean
index a937da29fa..291eedbb4c 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -338,4 +338,7 @@ namespace nat
     (le.refl a)
     (λ b₁ ih, le.trans !pred_le ih)
 
+  definition of_num [coercion] [reducible] (n : num) : ℕ :=
+  num.rec zero
+    (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 end nat