diff --git a/Game/Levels/AdvAddition/levels b/Game/Levels/AdvAddition/levels
index 9978205..970972f 100644
--- a/Game/Levels/AdvAddition/levels
+++ b/Game/Levels/AdvAddition/levels
@@ -4,3 +4,5 @@ h2 : x+5y=6
 ⊢ x=1
 
 ?
+
+example (x y : ℕ) (h1 : 2 * x + 3 * y = 5) (h2 : 4 * x + 5 * y = 9) : x = 1 := by
diff --git a/Game/Levels/LessOrEqual.lean b/Game/Levels/LessOrEqual.lean
index 6bdfc93..9eb2db3 100644
--- a/Game/Levels/LessOrEqual.lean
+++ b/Game/Levels/LessOrEqual.lean
@@ -3,6 +3,9 @@ import Game.Levels.LessOrEqual.L01le_refl
 import Game.Levels.LessOrEqual.L02zero_le
 import Game.Levels.LessOrEqual.L03le_succ_self
 import Game.Levels.LessOrEqual.L04le_zero
+import Game.Levels.LessOrEqual.L05le_trans
+import Game.Levels.LessOrEqual.L06le_antisymm
+import Game.Levels.LessOrEqual.L07le_total
 
 World "LessOrEqual"
 Title "≤ World"
diff --git a/Game/Levels/LessOrEqual/L02zero_le.lean b/Game/Levels/LessOrEqual/L02zero_le.lean
index 36b9bbc..4af1bb2 100644
--- a/Game/Levels/LessOrEqual/L02zero_le.lean
+++ b/Game/Levels/LessOrEqual/L02zero_le.lean
@@ -14,8 +14,11 @@ how to prove `a ≤ b` is to `use b - a`. See how you get on with this level,
 which proves that every number in the game is at least 0.
 "
 
-/-- If $x$ is a number, then $0 \\le x$. -/
-Statement le_refl (x : ℕ) : 0 ≤ x := by
+LemmaDoc MyNat.zero_le as "zero_le" in "≤" "
+`zero_le x` is a proof that `0 ≤ x`."
+
+/-- If $x$ is a number, then $0 \le x$. -/
+Statement zero_le (x : ℕ) : 0 ≤ x := by
   use x
   rw [zero_add]
   rfl
diff --git a/Game/Levels/LessOrEqual/L03le_succ_self.lean b/Game/Levels/LessOrEqual/L03le_succ_self.lean
index 29e5c3c..a0d46ab 100644
--- a/Game/Levels/LessOrEqual/L03le_succ_self.lean
+++ b/Game/Levels/LessOrEqual/L03le_succ_self.lean
@@ -10,14 +10,24 @@ LemmaDoc MyNat.le_succ_self as "le_succ_self" in "≤" "
 `le_succ_self x` is a proof that `x ≤ succ x`.
 "
 
-/-- If $x$ is a number, then $x \\le \\mathoperator{succ}(x)$. -/
-Statement le_succ_self (x : ℕ) : x ≤ succ x := by
+/-- If $x$ is a number, then $x \le \operatorname{succ}(x)$. -/
+Statement (x : ℕ) : x ≤ succ x := by
   use 1
   rw [succ_eq_add_one]
   rfl
 
 LemmaTab "≤"
 
+Conclusion "
+Here's a two-liner:
+```
+use 1
+exact succ_eq_add_one x
+```
+
+This works because `succ_eq_add_one x` is a proof of `succ x = x + 1`.
+"
+
 /-
 Introduction
 "
diff --git a/Game/Levels/LessOrEqual/L04le_zero.lean b/Game/Levels/LessOrEqual/L04le_zero.lean
index 3d285d8..fdc0973 100644
--- a/Game/Levels/LessOrEqual/L04le_zero.lean
+++ b/Game/Levels/LessOrEqual/L04le_zero.lean
@@ -12,24 +12,22 @@ LemmaDoc MyNat.le_zero as "le_zero" in "≤" "
 
 Introduction "
 In this level, our inequality is a *hypothesis*. We have not seen this before.
-
+The `rcases` tactic can be used to take `hx` apart.
 "
+
+LemmaDoc MyNat.le_zero as "le_zero" in "≤"
+"`le_zero x` is a proof of the implication `x ≤ 0 → x = 0`. "
+
 /-- If $x \leq 0$, then $x=0$. -/
 Statement le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by
+  Hint "Start with `cases hx with y hy`. You can get the funny pointy brackets with `\\<` and
+  `\\>`, or `\\<>` will give you both at once."
   cases hx with y hy
+  Hint "Now `y` is what you have to add to `x` to get `0`, and `hy` is the proof of this."
+  Hint (hidden := true) "You want to use `eq_zero_of_add_right_eq_zero`, which you already
+  proved, but you'll have to start with `symm at hy`."
   symm at hy
   apply eq_zero_of_add_right_eq_zero at hy
   exact hy
 
 LemmaTab "≤"
-
-/-
-Introduction
-"
-Because constanly rewriting `zero_add` and `add_zero` is a bit dull,
-let's unlock the `ring` tactic. This will prove any goal which is \"true
-in the language of ring theory\", for example `a + b + c = c + b + a`.
-It doesn't understand `succ` though, so use `succ_eq_add_one` in this
-level to get rid of it.
-"
--/
diff --git a/Game/Levels/LessOrEqual/L05le_trans.lean b/Game/Levels/LessOrEqual/L05le_trans.lean
new file mode 100644
index 0000000..2d6ca02
--- /dev/null
+++ b/Game/Levels/LessOrEqual/L05le_trans.lean
@@ -0,0 +1,49 @@
+import Game.Levels.LessOrEqual.L04le_zero
+
+World "LessOrEqual"
+Level 5
+Title "x ≤ y and y ≤ z implies x ≤ z"
+
+namespace MyNat
+
+Introduction "
+We have already proved that `x ≤ x`, i.e. that `≤` is *reflexive*. Now let's
+prove that it's *transitive*, i.e., that if `x ≤ y` and `y ≤ z` then `x ≤ z`.
+"
+
+LemmaDoc MyNat.le_trans as "le_trans" in "≤" "
+`le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.
+More precisely, it is a proof that `x ≤ y → (y ≤ z → x ≤ z)`. In words,
+If $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.
+
+## A note on associativity
+
+In Lean, `a + b + c` means `(a + b) + c`, because `+` is left associative. However
+`→` is right associative, meaning that `x ≤ y → y ≤ z → x ≤ z` means
+exactly that `≤` is transitive.
+"
+
+/-- If $x \leq y$ and $y \leq z$, then $x \leq z$. -/
+Statement le_trans (x y z : ℕ) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
+  Hint "If you start with `rcases hxy with ⟨a, ha⟩` then `ha` will be a proof that `y = x + a`.
+  If you want to instead *define* `y` to be `x + a` then you can do `rcases hxy with ⟨a, rfl⟩`.
+  This is a time-saving trick. "
+  rcases hxy with ⟨a, rfl⟩
+  rcases hyz with ⟨b, rfl⟩
+  use a + b
+  exact add_assoc x a b
+
+LemmaTab "≤"
+
+Conclusion "
+Here's a four line proof:
+```
+rcases hxy with ⟨a, rfl⟩
+rcases hyz with ⟨b, rfl⟩
+use a + b
+exact add_assoc x a b
+```
+
+A passing mathematician remarks that with reflexivity and transitivity out of the way,
+you have proved that `≤` is a *preorder* on `ℕ`.
+"
diff --git a/Game/Levels/LessOrEqual/L06le_antisymm.lean b/Game/Levels/LessOrEqual/L06le_antisymm.lean
new file mode 100644
index 0000000..b2918aa
--- /dev/null
+++ b/Game/Levels/LessOrEqual/L06le_antisymm.lean
@@ -0,0 +1,50 @@
+import Game.Levels.LessOrEqual.L05le_trans
+
+World "LessOrEqual"
+Level 6
+Title "x ≤ y and y ≤ x implies x = y"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_antisymm as "le_antisymm" in "≤" "
+`le_antisymm x y` is a proof that if `x ≤ y` and `y ≤ x` then `x = y`.
+"
+
+Introduction "
+This level asks you to prove *antisymmetry* of $\\leq$.
+In other words, if $x \\leq y$ and $y \\leq x$ then $x = y$.
+It's the trickiest one so far. Good luck!
+"
+
+/-- If $x \leq y$ and $y \leq x$, then $x = y$. -/
+Statement le_antisymm (x y : ℕ) (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
+  rcases hxy with ⟨a, rfl⟩
+  rcases hyx with ⟨b, hb⟩
+  rw [add_assoc] at hb
+  symm at hb
+  apply add_right_eq_self at hb
+  apply eq_zero_of_add_right_eq_zero at hb
+  rw [hb, add_zero]
+  rfl
+
+LemmaTab "≤"
+
+Conclusion "
+Here's my proof:
+```
+rcases hxy with ⟨a, rfl⟩
+rcases hyx with ⟨b, hb⟩
+rw [add_assoc] at hb
+symm at hb
+apply add_right_eq_self at hb
+apply eq_zero_of_add_right_eq_zero at hb
+rw [hb, add_zero]
+rfl
+```
+
+A passing mathematician remarks that with antisymmetry as well,
+you have proved that `≤` is a *partial order* on `ℕ`.
+
+The next level, the boss level of this world, is to prove
+that `≤` is a total order.
+"
diff --git a/Game/Levels/LessOrEqual/L07le_total.lean b/Game/Levels/LessOrEqual/L07le_total.lean
new file mode 100644
index 0000000..0af4df7
--- /dev/null
+++ b/Game/Levels/LessOrEqual/L07le_total.lean
@@ -0,0 +1,68 @@
+import Game.Levels.LessOrEqual.L06le_antisymm
+
+World "LessOrEqual"
+Level 7
+Title "x ≤ y or y ≤ x"
+
+namespace MyNat
+
+Introduction "
+This is I think the toughest level yet. We haven't talked about \"or\" at all,
+but here's everything you need to know.
+
+1) The notation for \"or\" is `∨`. You won't need to type it, but you can
+type it with `\\or`.
+
+2) If you have an \"or\" statement in the *goal*, then two tactics made
+progress: `left` and `right`. But don't choose a direction unless your
+hypotheses guarantee that it's the right one.
+
+3) If you have an \"or\" statement as a *hypothesis* `h`, then
+`rcases h with (h1 | h2)` will create two goals, one where you went left,
+and the other where you went right.
+"
+
+LemmaDoc MyNat.le_total as "le_total" in "≤" "
+`le_total x y` is a proof that `x ≤ y` or `y ≤ x`.
+"
+
+/-- If $x \leq y$ and $y \leq z$, then $x \leq z$. -/
+Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
+  induction y with d hd
+  right
+  exact zero_le x
+  rcases hd with (h1 | h2)
+  left
+  rcases h1 with ⟨e, rfl⟩
+  use e + 1
+  rw [succ_eq_add_one, add_assoc]
+  rfl
+  rcases h2 with ⟨e, rfl⟩
+  rcases e with ⟨f⟩
+  left
+  change d + 0 ≤ succ d
+  rw [add_zero]
+  use 1
+  exact succ_eq_add_one d
+  right
+  use a
+  rw [add_succ, succ_add, add_comm]
+  rfl
+
+
+
+
+LemmaTab "≤"
+
+Conclusion "
+Here's a four line proof:
+```
+rcases hxy with ⟨a, rfl⟩
+rcases hyz with ⟨b, rfl⟩
+use a + b
+exact add_assoc x a b
+```
+
+A passing mathematician remarks that with reflexivity and transitivity out of the way,
+you have proved that `≤` is a *preorder* on `ℕ`.
+"
diff --git a/Game/Levels/LessOrEqual/all_levels.lean b/Game/Levels/LessOrEqual/all_levels.lean
deleted file mode 100644
index 4472707..0000000
--- a/Game/Levels/LessOrEqual/all_levels.lean
+++ /dev/null
@@ -1,99 +0,0 @@
-import Game.Levels.AdvAddition.L11add_right_eq_self
-
-namespace MyNat
-
-def le (a b : ℕ) : Prop := ∃ c, b = a + c
-
-instance : LE MyNat := ⟨le⟩
-
-example (x : ℕ) : 0 ≤ x := by
-  use x -- **************** need `use` tactic
-  rw [zero_add]
-  rfl
-
-example (x : ℕ) : x ≤ x := by
-  use 0
-  rw [add_zero]
-  rfl
-
-example (x : ℕ) : x ≤ succ x := by
-  use 1
-  rw [succ_eq_add_one]
-  rfl
-
-example (x y : Nat) : x + y = 0 → x = 0 := by exact?
-
--- **TODO** ask on Zulip: why is this not called eq_zero_of_add_left_eq_zero ?
-#check Nat.eq_zero_of_add_eq_zero_left -- (h : n + m = 0) : m = 0
-
-#check add_right
-axiom eq_zero_of_add_eq_zero_right (x y : ℕ) (h : x + y = 0) : x = 0 -- ***************** need this
-
-example (x : ℕ) (h : x ≤ 0) : x = 0 := by
-  cases' h with n hn -- ************************ need `cases` tactic
-  rw [eq_comm] at hn -- ************************ ouch, need `rw` with iffs
-  apply eq_zero_of_add_eq_zero_right at hn
-  assumption
-
-example (x y z : ℕ) (h1 : x ≤ y) (h2 : y ≤ z) : x ≤ z := by
-  cases' h1 with n hn
-  cases' h2 with m hm
-  rw [hm, hn]
-  use n + m
-  rw [add_assoc]
-  rfl
-
-example (x y : ℕ) (h1 : x ≤ y) (h2 : y ≤ x) : x = y := by
-  cases' h1 with n hn
-  cases' h2 with m hm
-  rw [hm] at hn
-  rw [add_assoc] at hn
-  rw [eq_comm] at hn -- ***************** more rw with iff
-  apply add_right_eq_self at hn
-  apply add_eq_zero at hn
-  rw [hn, add_zero] at hm
-  assumption
-
-example (x y : ℕ) : x ≤ y ∨ y ≤ x := by
-  -- ******************************* need `∨`
-  induction x with d hd
-  left -- *********************** need `left`
-  use y
-  rw [zero_add]
-  rfl
-  cases' hd with h1 h2 -- ***************** cases on an or
-  cases' h1 with n hn -- ***************** cases on a prop
-  cases' n with n -- ******************* cases on a nat
-  change y = d + 0 at hn
-  rw [add_zero] at hn
-  right -- ***************************** need `right`
-  rw [hn]
-  use 1
-  rw [succ_eq_add_one]
-  rfl
-  rw [add_succ] at hn
-  left
-  rw [hn]
-  -- succ a ≤ succ b ↔ a ≤ b would have been handy here
-  rw [succ_eq_add_one, succ_eq_add_one]
-  use n
-  rw [add_right_comm]
-  rfl
-  right
-  cases' h2 with n
-  use n + 1
-  rw [succ_eq_add_one, h]
-  rw [add_assoc]
-  rfl
-
-
-
-#exit
-a) 0 ≤ x;
-b) x ≤ x;
-c) x ≤ S(x);
-d) If x ≤ 0 then x = 0.
-a) x ≤ x (reflexivity);
-b) If x ≤ y and y ≤ z then x ≤ z (transitivity);
-c) If x ≤ y and y ≤ x then x = y (antisymmetry);
-d) Either x ≤ y or y ≤ x (totality).