totem3/coq-prac こういうのをやることにした。 ただCoqの標準ライブラリからLemmaとTheoremを取り出してきただけ。 こんな初歩的なものなら簡単に証明できるだろ＼(^o^)／ と思っていたら、いきなりできない・・・ｗ Lemma le_n_0_eq n : n <= 0 -> 0 = n. …