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