Really nice tutorial on Coq's theorem proving facilities. It even covers Ltac which is rare for these kinds of tutorials.