algorithm world now looking good

Game/Levels/Algorithm/L04pred.lean

@@ -45,5 +45,5 @@ Statement (a b : ℕ) (h : succ a = succ b) : a = b := by
   rfl
 
 Conclusion
-"Let's now prove Peano's other axiom, `zero_ne_succ`.
+"Let's now prove Peano's other axiom, that successors can't be $0$.
 "

Game/Levels/Algorithm/L05is_zero.lean

@@ -52,7 +52,3 @@ Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
   rw [h]
   rw [is_zero_zero]
   tauto
-
-Conclusion
-"Let's now use these lemmas to prove
-"

Game/Levels/Algorithm/L06succ_ne_succ.lean

@@ -14,14 +14,16 @@ Every natural is either `0` or `succ n` for some `n`. Here is an algorithm
 which, given two naturals `a` and `b`, returns the answer to \"does `a = b`?\"
 
 *) If they're both `0`, return \"yes\".
+
 *) If one is `0` and the other is `succ n`, return \"no\".
+
 *) If `a = succ m` and `b = succ n`, then return the answer to \"does `m = n`?\"
 
 Let's prove that this algorithm always gives the correct answer. The proof that
 `0 = 0` is `rfl`. The proof that `0 ≠ succ n` is `zero_ne_succ n`, and the proof
 that `succ m ≠ 0` is `succ_ne_zero m`. The proof that if `h : m = n` then
 `succ m = succ n` is `rw [h]` and then `rfl`. The next level is a proof of the one
-remaining case.
+remaining case: if `a ≠ b` then `succ a ≠ succ b`.
 "
 
 TacticDoc «have» "

Game/Levels/Algorithm/L07decide.lean

@@ -58,5 +58,3 @@ between two naturals. Run it with the `decide` tactic.
 /-- $20+20=40$. -/
 Statement : (20 : ℕ) + 20 = 40 := by
   decide
-
--- need tacticdoc

Game/Levels/Algorithm/L08decide2.lean

@@ -0,0 +1,21 @@
+import Game.Levels.Algorithm.L07decide
+
+World "Algorithm"
+Level 8
+Title "decide again"
+
+LemmaTab "Peano"
+
+namespace MyNat
+
+Introduction
+"
+We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.
+"
+
+/-- $2+2 \neq 5.$ -/
+Statement : (2 : ℕ) + 2 ≠ 5 := by
+  decide
+
+Conclusion "Congratulations! You've finished Algorithm World. These algorithms
+will be helpful for you in Even-Odd World."