Original writeup (https://tcode2k16.github.io/blog/posts/2020-11-22-a-hands-on-introduction-to-coq/).