From 2d5257fdc130ede3bb63fb345c441ae876ec0580 Mon Sep 17 00:00:00 2001
From: Madjosz <28844868+Madjosz@users.noreply.github.com>
Date: Mon, 30 Oct 2023 10:10:51 +0100
Subject: [PATCH] Fix #37: theorem comment Algorithm world, level 6

---
 Game/Levels/Algorithm/L06is_zero.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Game/Levels/Algorithm/L06is_zero.lean b/Game/Levels/Algorithm/L06is_zero.lean
index b417fd5..97992d7 100644
--- a/Game/Levels/Algorithm/L06is_zero.lean
+++ b/Game/Levels/Algorithm/L06is_zero.lean
@@ -42,7 +42,7 @@ LemmaDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Peano"
 
 NewLemma MyNat.is_zero_zero MyNat.is_zero_succ
 
-/-- If $\operatorname{succ}(a)=\operatorname{succ}(b)$ then $a=b$. -/
+/-- $\operatorname{succ}(a) \neq 0$. -/
 Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
   Hint "Start with `intro h` (remembering that `X ≠ Y` is just notation
   for `X = Y → False`)."