Honestly, part of the reason that proof assistants are focused on proving programs is precisely because of our very limited understanding of how to actually represent mathematics in formal logical systems, as opposed to doing it in principle.
It turns out that program proof is basically applied metamathematics (i.e., verification of imperative programs is model theory, and verification of functional programs is structural proof theory) and this is the one area of mathematics where folks have really fully worked out in full detail how to represent what they're doing in formal logical systems. So the focus on program proof is partly making a virtue of necessity! (It's also because those of us in this area really like both programming and mathematics, and this is a great way to combine them...)
The number of people who know how to do real math in proof assistants and explain it to others can probably be counted on your fingers. A pair of suggestions to add to your list follows:
John Harrison wrote a recent book, Handbook of Practical Logic and Automated Reasoning, which people I trust rave about. It's a guide to all the decision procedures (e.g., SAT solving, unification, Presburger arithmetic, Groebner bases, etc.) that you need to raise the level of formal proof to a decent level of abstraction, together with their implementations in the HOL/Light system.
George Gonthier (who formally proved the Four Color Theorem in Coq) is currently working on formalzing the Feit-Thompson (aka Odd Order) Theorem of finite group theory. As part of this work, he and his collaborators are developing the more substantial libraries and proof automatation to support a more mathematical (as opposed to logical) style of reasoning in Coq. The guides to this work are "A Modular Formalisation of Finite Group Theory" and their Mathematical Components Library.
