From 3e62dcbbefdb5f20cdff47daf25257f174c3cf34 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 10 Oct 2023 20:01:50 +0900
Subject: [PATCH] =?UTF-8?q?trivial=20=E3=81=AE=E8=AA=AC=E6=98=8E=E3=82=92?=
 =?UTF-8?q?=E6=9B=B4=E6=96=B0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

aesop を推薦する
---
 src/trivial.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/trivial.md b/src/trivial.md
index 01f343a7..d0b43359 100644
--- a/src/trivial.md
+++ b/src/trivial.md
@@ -7,3 +7,5 @@
 ```lean
 {{#include ../Examples/Trivial.lean}}
 ```
+
+普段の数学でいう「自明」な命題は `trivial` では示せないことがほとんどだと思います．[aesop](./aesop.md) を試してみてください．
\ No newline at end of file