Add some lemmas and tactics for removing isos

This is the main tactic used to prove that lax comma categories are
precategories.  Unfortunately, it's sometimes rather slow.  It could
probably benefit from reflective automation.

This closes #383
Vastly simplify the helper-tactics in Category/Morphisms.v

We don't actually need all of those; I was being stupid with
associativity.
Add some helper lemmas about [commutes]
Merge pull request #384 from JasonGross/misc-lemmas

Miscellaneous category theory lemmas