From f56250d41e2dae0f5803e7f1cbbbe45e6551c2ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Jan 2017 14:17:56 -0800 Subject: [PATCH] chore(library/init/data/nat/lemmas): mark nat.add_zero as protected --- library/init/data/nat/lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 438cc0c314..ae1a88b314 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -20,7 +20,7 @@ lemma succ_add : ∀ n m : ℕ, (succ n) + m = succ (n + m) lemma add_succ : ∀ n m : ℕ, n + succ m = succ (n + m) := λ n m, rfl -lemma add_zero : ∀ n : ℕ, n + 0 = n := +protected lemma add_zero : ∀ n : ℕ, n + 0 = n := λ n, rfl lemma add_one_eq_succ : ∀ n : ℕ, n + 1 = succ n :=