3 ms·Mathematical Components: formalized mathematics for the Coq system3 points by adamnemecek 8y agoanonlastname 8y agoIIRC, the only reason mathcomp isn't in the Coq standard library is because the license isn't free.