add le_one and le_two to <= levels

Game/Levels/LessOrEqual.lean

@@ -7,6 +7,9 @@ import Game.Levels.LessOrEqual.L05le_zero
 import Game.Levels.LessOrEqual.L06le_antisymm
 import Game.Levels.LessOrEqual.L07or_symm
 import Game.Levels.LessOrEqual.L08le_total
+import Game.Levels.LessOrEqual.L09le_of_succ_le_succ
+import Game.Levels.LessOrEqual.L10le_one
+import Game.Levels.LessOrEqual.L11le_two
 
 World "LessOrEqual"
 Title "≤ World"

Game/Levels/LessOrEqual/L08le_total.lean

@@ -11,7 +11,13 @@ LemmaDoc MyNat.le_total as "le_total" in "≤" "
 "
 
 Introduction "
-This is I think the toughest level yet.
+This is I think the toughest level yet. Tips: if `a` is a number
+then `cases a with b` will split into cases `a = 0` and `a = succ b`.
+And don't go left or right until your hypotheses guarantee that
+you can prove the resulting goal!
+
+I've left hidden hints; if you need them, retry from the beginning
+and click on \"Show more help!\"
 "
 
 /-- If $x$ and $y$ are numbers, then either $x \leq y$ or $y \leq x$. -/
@@ -51,10 +57,5 @@ Very well done.
 A passing mathematician remarks that with you've just proved that `ℕ` is totally
 ordered.
 
-The next step in the development of order theory is to develop
-the theory of the interplay between `≤` and multiplication.
-If you've already done multiplication world, step into
-advanced multiplication world (once I've written it...)
+The final few levels in this world are much easier.
 "
-
--- **TODO** fix this

Game/Levels/LessOrEqual/L09le_of_succ_le_succ.lean

@@ -0,0 +1,39 @@
+import Game.Levels.LessOrEqual.L08le_total
+
+World "LessOrEqual"
+Level 9
+Title "succ x ≤ succ y → x ≤ y"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_of_succ_le_succ as "le_of_succ_le_succ" in "≤" "
+`le_of_succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`.
+"
+
+Introduction "
+The last goal in this world is to prove which numbers are `≤ 2`.
+This lemma will be helpful for that.
+"
+
+/-- If $\operatorname{succ}(x) \leq \operatorname{succ}(y)$ then $x \leq y$. -/
+Statement le_of_succ_le_succ (x y : ℕ) (hx : succ x ≤ succ y) : x ≤ y := by
+  cases hx with d hd
+  use d
+  rw [succ_add] at hd
+  apply succ_inj at hd
+  exact hd
+
+Conclusion "
+Here's my proof:
+```
+cases hx with d hd
+use d
+rw [succ_add] at hd
+apply succ_inj at hd
+exact hd
+```
+
+This lemma can be helpful for the next two levels.
+"

Game/Levels/LessOrEqual/L10le_one.lean

@@ -0,0 +1,46 @@
+import Game.Levels.LessOrEqual.L09le_of_succ_le_succ
+World "LessOrEqual"
+Level 10
+Title "x ≤ 1"
+
+LemmaTab "≤"
+
+namespace MyNat
+
+LemmaDoc MyNat.le_one as "le_one" in "≤" "
+`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`.
+"
+
+Introduction "
+We've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`.
+Now we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`.
+"
+
+/-- If $x \leq 1$ then either $x = 0$ or $x = 1$. -/
+Statement le_one (x : ℕ) (hx : x ≤ 1) : x = 0 ∨ x = 1 := by
+  cases x with y
+  left
+  rfl
+  rw [one_eq_succ_zero] at hx ⊢
+  apply le_of_succ_le_succ at hx
+  apply le_zero at hx
+  rw [hx]
+  right
+  rfl
+
+Conclusion "
+Here's my proof:
+```
+cases x with y
+left
+rfl
+rw [one_eq_succ_zero] at hx ⊢
+apply le_of_succ_le_succ at hx
+apply le_zero at hx
+rw [hx]
+right
+rfl
+```
+
+If you solved this level then you should be fine with the next level!
+"

Game/Levels/LessOrEqual/L11le_two.lean

@@ -0,0 +1,48 @@
+import Game.Levels.LessOrEqual.L10le_one
+World "LessOrEqual"
+Level 11
+Title "le_two"
+
+namespace MyNat
+
+LemmaTab "012"
+
+LemmaDoc MyNat.le_two as "le_two" in "≤" "
+`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`.
+"
+
+Introduction "
+We'll need this lemma to prove that two is prime!
+
+You'll need to know that `∨` is right associative. This means that
+`x = 0 ∨ x = 1 ∨ x = 2` actually means `x = 0 ∨ (x = 1 ∨ x = 2)`.
+"
+
+/-- If $x \leq 2$ then $x = 0$ or $1$ or $2$. -/
+Statement le_two (x : ℕ) (hx : x ≤ 2) : x = 0 ∨ x = 1 ∨ x = 2 := by
+  cases x with y
+  left
+  rfl
+  cases y with z
+  right
+  left
+  rw [one_eq_succ_zero]
+  rfl
+  rw [two_eq_succ_one, one_eq_succ_zero] at hx ⊢
+  apply le_of_succ_le_succ at hx
+  apply le_of_succ_le_succ at hx
+  apply le_zero at hx
+  rw [hx]
+  right
+  right
+  rfl
+
+
+Conclusion "
+Nice!
+
+The next step in the development of order theory is to develop
+the theory of the interplay between `≤` and multiplication.
+If you've already done Multiplication World, step into
+Advanced Multiplication World (once I've written it...)
+"