From 86d7904ea7529254bb845d15efd342a1be2cbaf4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Jul 2019 13:13:04 -0700
Subject: [PATCH] chore(library/init/data/nat/basic): avoid empty set of
 equations

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

diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index 0693c8ab39..98b9f6f354 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -258,7 +258,8 @@ succLeSucc (zeroLe n)
 def succPos := zeroLtSucc
 
 theorem notSuccLeZero : ∀ (n : Nat), succ n ≤ 0 → False
-.
+| 0     h := nomatch h
+| (n+1) h := nomatch h
 
 theorem notLtZero (n : Nat) : ¬ n < 0 :=
 notSuccLeZero n