From b18d5667c2a49129409e4f8b894aeee4f133be79 Mon Sep 17 00:00:00 2001
From: Naman Chhawchharia <13197426+nvchhawch@users.noreply.github.com>
Date: Thu, 19 Oct 2023 11:56:38 -0400
Subject: [PATCH] Add `zero_ne_succ`

---
 Game/Levels/Implication/L09zero_ne_succ.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Game/Levels/Implication/L09zero_ne_succ.lean b/Game/Levels/Implication/L09zero_ne_succ.lean
index ecb1216..8957a61 100644
--- a/Game/Levels/Implication/L09zero_ne_succ.lean
+++ b/Game/Levels/Implication/L09zero_ne_succ.lean
@@ -18,6 +18,8 @@ Here `False` is a generic false statement. This means that
 you can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`.
 "
 
+NewLemma MyNat.zero_ne_succ
+
 Introduction "
 As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to
 introduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.