Transitivity

scm 老師把 MSS 寫到剩兩個 lemma（實在太強了！），讓我們練習證明。我證了一下讓 program check，很高興就廣播出去，然後很快就後悔了 XD。因為第一個 lemma 的證明我用窮舉法，但因為 less-than 有 transitivity 而漏掉兩個不可能發生的 cases。這樣程式就有瑕疵，因為形式上那個 lemma 只是 partially correct（可是 Agda 對此從不抱怨）。真的要做應該還是得證明整數的 transitivity，可是很麻煩 XD。

--
凡事三思而後行 XD。

---

整個狀況想一想實在很詭異 XD。

---

現在 scm 老師把整個結果發佈在他的 blog 上啦！