Transitivity

Now that tactics like `symmetry` are defined in Coq-land in the stdlib, thanks to Pierre-Marie Pédrot, we can define our own versions that, after unfolding, result in proofs using things like `concat`.  I've replaced `apply symmetry` with `symmetry` and `path_via` with `transitivity` (appending `auto with path_hints` to the cases that need it).  I've removed the `path_via` tactic.  If we want to keep `path_via`, I can strip the commit that removes `path_via` and inserts explicit `auto with path_hints`.

A question: Do we want to mark the relevant constants as auto-unfolding, so that when we `simpl`, proofs built will `transitivity` and `symmetry` will unfold to uses of `concat` and `inverse`?