First contact with Coq

I've started to look a bit into Coq, beginning with Coq in a Hurry. It begins nice enough, but then in section 3 there's a proof that for all propositions a and b, a and b implies b and a. I didn't understand a thing. Well, one bit or another, judging by previous contacts with systems for first order logic, but the tactics, and the organization of the proof, it all flew over my head. Just by reading the material it was hard to discern what was I supposed to input to get the same result. Then there are two paragraphs about the tactics, and a table. I can't imagine how I would use it right now.

But that's ok, I'm sure I'll understand it better later. There's the Coq Tutorial and a bit more of material to get into. Then I'll post about it later, if I don't get lazy. It's bound to be truly exciting stuff about the Calculus of Inductive Constructions and dependent type theory. Great subject to draw upon for chitchat at cocktail parties.