進捗あまりない。
update · 702639b · totem3/coq-prac · GitHub
全然わからんのでもうImportしたのを使って証明せずに進めているｗ
できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。
こうなってくると、今後まともにやっていくうえで大事なのはSearchを使いこなすことのような気がしてくるんだけど、不等号系が全然SearchRewriteとか使っても出てこない
このあたりがよくわからない。次使いこなすべきはSearchかなと思った
n <= m -> ~ m < nとかFalseの証明がでてきたけど、これがやっぱりわからない。
Searchを使いこなせるようになるのと、矛盾を示せるようになりたい
