Add zero_ne_succ

leanprover-community · Oct 19, 2023 · b18d566 · b18d566
1 parent 2d26496
commit b18d566
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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`.