slides: www.math.ias.edu/vladimir/files/Anand_ICMS2016.pdf
Also, Sec 2.2 of the following tech report explains the core ideas behind the design of this library: http://www.nuprl.org/html/verification/verification.pdf
There is also a de-bruijn version of the above ideas. See termsDB.v
Installation:
make
sudo make install