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/ae54d9b27f7afa8cabb7cc84c425...

couldn't get the link to work in the lean-web-editor though.