From 5daf1986e7bdbdd32f4b7627e384bcee414faf61 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Nov 2016 10:54:28 -0800
Subject: [PATCH] feat(library/init/nat): add nat.zero = zero (rfl) lemma

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

diff --git a/library/init/nat.lean b/library/init/nat.lean
index cc150f4113..87495229e6 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -59,6 +59,9 @@ def {u} repeat {α : Type u} (f : ℕ → α → α) : ℕ → α → α
 instance : inhabited ℕ :=
 ⟨nat.zero⟩
 
+@[simp] lemma nat_zero_eq_zero : nat.zero = 0 :=
+rfl
+
 /- properties of inequality -/
 
 @[refl] protected def le_refl : ∀ a : ℕ, a ≤ a :=