better LemmaTab for le_succ_self

2023-12-22 15:46:10 +00:00
parent 6f8d7062db
commit 4219e68302
1 changed files with 1 additions and 1 deletions
--- a/Game/Levels/LessOrEqual/L03le_succ_self.lean
+++ b/Game/Levels/LessOrEqual/L03le_succ_self.lean
@@ -19,7 +19,7 @@ Statement le_succ_self (x : ℕ) : x ≤ succ x := by
  rw [succ_eq_add_one]
  rfl

-LemmaTab "≤"
+LemmaTab "+"

 Conclusion "
 Here's a two-liner: