Proof assistants for mathematics
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.
I am interested in the same kind of stuff. This article tells about work done to formalize group representation theory in Coq. In particular, they formalize the proof of Maschke's theorem (that $F[G]$ is semisimple when $G$ is a finite group).
Some links to math courses using Coq are listed in Cocorico.
Are you aware of the Archive of Formal Proof for Isabelle? It's a collection of formalized mathematics (and some program verification). Reading the papers there, and browsing the Isabelle theory file sources is a good way to learn.
The Isar tutorial is also a good place to look, if you want to write proofs that look like informal mathematics (as opposed to tactic style). It's quite hard to get the hang of at first (mostly due to lack of documentation), but once you get it, it's a lot easier to work with than plain lists of tactics.
If you're wanting to formalise anything with name binders (lambda-calculus, FOL, programming languages, pi-calculus, etc.) you should also check out the Nominal package for Isabelle which again helps with abstracting the proofs.