Merge pull request #32 from nvchhawch/main

Fix accidental removal of `zero_ne_succ`
leanprover-community · Oct 20, 2023 · 26512db · 26512db
2 parents 2d26496 + b18d566
commit 26512db
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`.