There are lots more places to learn about Coq.
The Coq'Art book and website. The website contains examples and exercises.
Certified Programming with Dependent Types, a textbook in progress by Adam Chlipala
Materials from the Using Proof Assistants for Programming Language Research tutorial.
Materials from the course Software foundations.
Materials from the Coq summer school Modelling and verifying algorithms in Coq: an introduction.
- Materials for courses in French:
The Coq-Club mailing list, subscription information and official archive
Coq IRC channel: irc://irc.freenode.net/#coq
See also: Resources for Coq Newbies