diff --git a/Game/Levels/AdvAddition/Level_5.lean b/Game/Levels/AdvAddition/Level_5.lean
deleted file mode 100644
index 76f0a50..0000000
--- a/Game/Levels/AdvAddition/Level_5.lean
+++ /dev/null
@@ -1,81 +0,0 @@
-import Game.Levels.AdvAddition.Level_4
-
-
-
-World "AdvAddition"
-Level 5
-Title "add_right_cancel"
-
-open MyNat
-
-Introduction
-"
-The theorem `add_right_cancel` is the theorem that you can cancel on the right
-when you're doing addition -- if `a + t = b + t` then `a = b`.
-"
-
-/-- On the set of natural numbers, addition has the right cancellation property.
-In other words, if there are natural numbers $a, b$ and $c$ such that
-$$ a + t = b + t, $$
-then we have $a = b$. -/
-Statement MyNat.add_right_cancel
-    (a t b : ℕ) : a + t = b + t → a = b := by
-  Hint (hidden := true) "You can either start with `induction t` or with
-  `intro` and you will have to do the other one afterwards."
-  Branch
-    intro h
-    Hint "I'd recommend now induction on `t`. Don't forget that `rw [add_zero] at h` can be used
-    to do rewriting of hypotheses rather than the goal."
-    induction t with d hd
-    · Hint "You might have noticed an old `{h}✝` floating
-      around in your assumptions. `x✝` marks variables that can't be used
-      anymore because a new variable got assigned the name `x`.
-      In your case that is because `induction` deleted the old `{h}` when
-      it created the `t=0` (or later `succ t`) variants. Just ignore the
-      `{h}✝`."
-      rw [add_zero] at h
-      rw [add_zero] at h
-      exact h
-    · Hint "You might have noticed an old `{h}✝` floating
-      around in your assumptions. `x✝` marks variables that can't be used
-      anymore because a new variable got assigned the name `x`.
-      In your case that is because `induction` deleted the old `{h}` when
-      it created the `succ t` variant. Just ignore the `{h}✝`."
-      Branch
-        simp at h
-        exact hd h
-      apply hd
-      rw [add_succ] at h
-      rw [add_succ] at h
-      exact succ_inj h
-  induction t with d hd
-  · Hint (hidden := true) "You want to look at `intro`."
-    Branch
-      simp
-    intro h
-    rw [add_zero] at h
-    rw [add_zero] at h
-    exact h
-  · Hint "Since you called `induction t` first, you now have to call
-    `intro` on each of the subgoals."
-    Hint (hidden := true) "You want to look at `intro`"
-    Branch
-      simp
-      exact hd
-    intro h
-    apply hd
-    rw [add_succ] at h
-    rw [add_succ] at h
-    Hint (hidden := true) "At this point `succ_inj` might be useful."
-    exact succ_inj h
-
-
--- TODO: Display at this level after induction is confusing: old assumption floating in context
-
-LemmaTab "Add"
-DisabledTactic simp
-
-Conclusion
-"
-
-"
diff --git a/Game/Levels/AdvAddition/Level_6.lean b/Game/Levels/AdvAddition/Level_6.lean
deleted file mode 100644
index ed3c788..0000000
--- a/Game/Levels/AdvAddition/Level_6.lean
+++ /dev/null
@@ -1,43 +0,0 @@
-import Game.Levels.AdvAddition.Level_5
-
-
-World "AdvAddition"
-Level 6
-Title "add_left_cancel"
-
-open MyNat
-
-Introduction
-"
-The theorem `add_left_cancel` is the theorem that you can cancel on the left
-when you're doing addition -- if `t + a = t + b` then `a = b`.
-"
-
-/-- On the set of natural numbers, addition has the left cancellation property.
-In other words, if there are natural numbers $a, b$ and $t$ such that
-$$ t + a = t + b, $$
-then we have $a = b$. -/
-Statement MyNat.add_left_cancel
-    (t a b : ℕ) : t + a = t + b → a = b := by
-  Branch
-    induction t
-    · simp
-    · simp
-      exact n_ih
-  Hint "There is a three-line proof which ends in `exact add_right_cancel a t b` (or even
-  `exact add_right_cancel _ _ _`); this
-  strategy involves changing the goal to the statement of `add_right_cancel` somehow."
-  rw [add_comm]
-  rw [add_comm t]
-  Hint "Now that looks like `add_right_cancel`!"
-  Hint (hidden := true) "`exact add_right_cancel` does not work. You need
-  `exact add_right_cancel a t b` or `exact add_right_cancel _ _ _`."
-  exact add_right_cancel a t b
-
-LemmaTab "Add"
-DisabledTactic simp
-
-Conclusion
-"
-
-"