Make `compose` a notation rather than a definition

This makes life a lot easier; we don't have to be constantly unfolding it, and we can avoid `Local Arguments compose /.` and `simpl rewrite` in lots of places.
I wrote the code assuming that `cbv beta` was a safe operation to do whenever, and wherever, and it wouldn't break patterns.  I should go to sleep nowish, but I've tracked the issue back to `left_associate_compose_in`, which should give you the lemma `fun h => (h o f) o g`, but is instead giving `fun h x => h (f (g x))`.  It might be possible to rework the tactics so they don't rely on this assumption.