For those unaware, one of the best resources to learn Rocq: https://softwarefoundations.cis.upenn.edu/