This question is related to (maybe even the same in intent as) Question 1017, but none of the answers seem to address what I'm looking for.

There are a lot of resources available for people who want to use proof assistants like Coq, Isabelle, …, to prove properties about programs—and that's no surprise, since a lot of the development of these programs is done by computer scientists. However, I am interested in resources, and especially in course materials (because I'm trying to put together an independent study for a CS student), involving the use of proof assistants to prove mathematical statements—see the work of Hales and Weedijk for examples. Does anyone know of any such?