The mathematical components library is an extensive library of formalized mathematics built using the ssreflect extension for the coq system.