I taught myself the rudiments of Coq on the train back. Addition of natural numbers is commutative, in case you were unsure. I have to say, I do see why people like its interactive proof-building mode. I am not sure how I feel about tactics, tacticals, etc. It makes for a lot of different languages to learn, most of which don't feel very principled. Obviously the advantage is that sometimes your proof just gets proved faster, but eh. It feels similar to arguments about laziness in programming languages --- how it can make your program run faster, but can make for less predictable performance.
There are some things that confuse me a bit about what the difference between Set and Prop really is, and the difference between parametrized induction type families and inductive definitions of things arrowing into types, the latter which seemed reminiscent of a similar potentially confusing point in Agda. But mostly it seemed like an ok system except for the glaring lack of direct Twelfish support of HOAS. Some day I'll have to figure out how I feel about the whole Washburn/Weirich/Chlipala/Atkey world of PHOAS.