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 agree that `fun f => g o f` is more readable, but I’d still vote for `Notation compose := (fun g f x => g (f x)).` since it allows both versions.

Generally, it’s a bit counter-intuitive having notations that look like identifiers, and behave like them most of the time but not all (e.g. if they can’t be used partially applied). I think I just about agree that in this case it’s worth it for the benefits, but it’s still worth trying to minimise the counter-intuitiveness.

Little exceptions-to-the-rules like this are imperceptible individually, but as they accumulate, they quickly raise the barrier-to-entry for understanding the library.