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