The Mathematical Components library for Coq has its origins in the formal proof of the Four Colour Theorem. Since then it has grown to cover many areas of mathematics and has been used for large scale projects like the formal proof of the Odd Order Theorem.
The library is written using the Ssreflect proof language that is an integral part of the distribution.
Each source files features a documentation header which describes the concepts and notations introduced in that file. The coqdoc presentation of the source files can be browsed online.
The library graph can be browsed interactively.
The Ssreflect language comes with a dedicated reference manual.
We also wrote a book introducing the techniques for writing algorithms and proofs and describing the design ideas of the library.
Interested? Subscribe to the ssreflect mailing list and let us know what you are using our libraries for, ask questions, etc. You can also browse the archives of the list or consult the general information page.