notation for declaring a function non-expansive

I suggest having a notation for a function being non-expansive, similar to how we have notation for contractiveness. This makes the common case (unary non-expansive functions) easier to read.