fix typo in statement of le_total

2023-10-24 17:55:54 +01:00
parent 6f7f99798e
commit 4d7a1c99c1
1 changed files with 1 additions and 1 deletions
--- a/Game/Levels/LessOrEqual/L08le_total.lean
+++ b/Game/Levels/LessOrEqual/L08le_total.lean
@@ -14,7 +14,7 @@ Introduction "
 This is I think the toughest level yet.
 "

-/-- If $x \leq y$ and $y \leq z$, then $x \leq z$. -/
+/-- If $x$ and $y$ are numbers, then either $x \leq y$ or $y \leq x$. -/
 Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
  Hint (hidden := true) "Start with `induction y with d hd`."
  induction y with d hd