From f9b62c53e6cedf922026c8b944d1647df2c93c2a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Sep 2014 19:50:15 -0700
Subject: [PATCH] feat(library/data/nat): add nat.is_inhabited theorem

---
 library/data/nat/basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index edcd4e3a17..d0b1023bfb 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -8,6 +8,7 @@
 -- Basic operations on the natural numbers.
 
 import logic data.num tools.tactic struc.binary tools.helper_tactics
+import logic.classes.inhabited
 
 open tactic binary eq_ops
 open decidable (hiding induction_on rec_on)
@@ -36,6 +37,8 @@ nat.rec H1 H2 a
 definition rec_on [protected] {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
 nat.rec H1 H2 n
 
+theorem is_inhabited [protected] [instance] : inhabited nat :=
+inhabited.mk zero
 
 -- Coercion from num
 -- -----------------