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.
The Coq-Club mailing list, subscription information and official archive
Coq IRC channel: irc://irc.freenode.net/#coq
See also: Resources for Coq Newbies