Nice writeup, been a while since I had used coq, it was nice to try and work it out from memory, but be able to refer back to your post when I got stuck. Also

Nice writeup, been a while since I had used coq, it was nice to try and work it out from memory, but be able to refer back to your post when I got stuck. Also threw together a tiny lean proof without tactics, figured i would post a link to it to avoid spoilers. https://gist.github.com/ratmice/ae54d9b27f7afa8cabb7cc84c42550e0 https://gist.github.com/ratmice/ae54d9b27f7afa8cabb7cc84c425... couldn't get the link to work in the lean-web-editor though.