diff --git a/Game/Levels/AdvAddition/L01ne_succ_self.lean b/Game/Levels/AdvAddition/L01ne_succ_self.lean
index 3ffdc22..c487432 100644
--- a/Game/Levels/AdvAddition/L01ne_succ_self.lean
+++ b/Game/Levels/AdvAddition/L01ne_succ_self.lean
@@ -15,6 +15,9 @@ which is a warm-up to see if you remember `zero_ne_succ`
 and `succ_inj`, and how to use the `apply` tactic.
 "
 
+LemmaDoc MyNat.ne_succ_self as "ne_succ_self" in "≤" "
+`ne_succ_self n` is the proof that `n ≠ succ n`."
+
 /-- $n\neq\operatorname{succ}(n)$. -/
 Statement ne_succ_self (n : ℕ) : n ≠ succ n := by
   Hint "Start with `induction`."
diff --git a/Game/Levels/LessOrEqual/L03le_succ_self.lean b/Game/Levels/LessOrEqual/L03le_succ_self.lean
index a847473..c447094 100644
--- a/Game/Levels/LessOrEqual/L03le_succ_self.lean
+++ b/Game/Levels/LessOrEqual/L03le_succ_self.lean
@@ -13,7 +13,7 @@ LemmaDoc MyNat.le_succ_self as "le_succ_self" in "≤" "
 NewLemma MyNat.le_succ_self
 
 /-- If $x$ is a number, then $x \le \operatorname{succ}(x)$. -/
-Statement (x : ℕ) : x ≤ succ x := by
+Statement le_succ_self (x : ℕ) : x ≤ succ x := by
   use 1
   rw [succ_eq_add_one]
   rfl