Type Classes for Mathematical Formalizations in Coq - Matthieu Sozeau