I recommend reading the first before the second, although sometimes pages from CPDT show up in Google when you have a question. Also don’t hesitate to check out the Coq reference manual (https://coq.inria.fr/distrib/current/refman/), although it will be overwhelming at first since it’s very pedantic and detailed, it becomes very useful once you have a basic understanding of Coq (like from reading the above).
The article skipped the most well-known and important books! (at least from my circle)
Software Foundations: https://softwarefoundations.cis.upenn.edu/
Certified Programming with Dependent Types (CPDT): http://adam.chlipala.net/cpdt/
I recommend reading the first before the second, although sometimes pages from CPDT show up in Google when you have a question. Also don’t hesitate to check out the Coq reference manual (https://coq.inria.fr/distrib/current/refman/), although it will be overwhelming at first since it’s very pedantic and detailed, it becomes very useful once you have a basic understanding of Coq (like from reading the above).