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`.