Mathematics Formalized in Coq
There is a great deal of mathematics already formalized in Coq. Some of the material is available in the StandardLibrary or in the Coq's repository of user contributions.
Top100MathematicalTheoremsInCoq: a list of theorems among the Top 100 Mathematical Theorems that are formalised in Coq (see also http://www.cs.ru.nl/~freek/100/).
CoRN : a large library of formalised mathematics built on top of Coq
Software Verified in Coq
Sorting
Algorithm 
Formalisation available from 
Quicksort 

Treesort 

Insertion sort 

Selection sort 

Maximum sort 

Heapsort 

Mergesort 