trivial の説明を更新

aesop を推薦する
lean-ja · Oct 10, 2023 · 3e62dcb · 3e62dcb
1 parent 4f5531f
commit 3e62dcb
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/trivial.md b/src/trivial.md
@@ -7,3 +7,5 @@
 ```lean
 {{#include ../Examples/Trivial.lean}}
 ```
+
+普段の数学でいう「自明」な命題は `trivial` では示せないことがほとんどだと思います．[aesop](./aesop.md) を試してみてください．