Looking into the Software Foundations book a little bit. Interesting stuff, but seems like it would take a while to get competent with Rocq. Giving it a look though, as I've wanted to check out proof software for a while now.