Setting up Coq, Ssreflect and Proof General on OS X - quanttype

Previously I've used CoqIDE to interact with Coq, because I figured out it'd be tricky to set up Proof General. Proof General the Emacs interface to Coq and other interactive theorem provers. This time I decided to take the PG route and turns out it's really easy if you're using Homebrew!