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