If you’re interested, here is my Coq tutorial.

http://michaeldnahas.com/doc/nahas_tutorial.html

It has been mentioned on HN before (multiple times).

https://news.ycombinator.com/item?id=21625852