This is a wonderful book and I recommend it to anybody learning Coq. The mathematical components project has made (and continues to make) great strides when it

This is a wonderful book and I recommend it to anybody learning Coq. The mathematical components project has made (and continues to make) great strides when it comes to formalizing research level mathematics. Before this book, there was only a small manual for ssreflect and information scattered throughout a dozen research papers. It's good to finally see more of a focus on documentation, since there are many people in the community who could benefit from using mathcomp instead of developing their own implementation of common mathematical structures.