Merge pull request #39 from Madjosz/patch-1

Fix #37: theorem comment Algorithm world, level 6
leanprover-community · Nov 1, 2023 · 9941e69 · 9941e69
2 parents d05c749 + 2d5257f
commit 9941e69
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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`)."