Type Classes for Mathematical Formalizations in Coq