It's certainly a nice solution, but OP's solution has the nice property of working directly on a universality definition, which makes the argument more general. For example, the universality argument also works for the infimum and gcd operations.

> For example, the universality argument also works for the infimum and gcd operations.

I've been thinking about this and I don't see how the argument can possibly work for the infimum operation. The problem is that infimum is necessarily a unary operation -- it doesn't make any sense to consider it to have multiple arguments.

Consider the open interval (1,2). The infimum is 1. But 1 is not contained in the interval. And because 1 is not contained within the interval, _if_ infimum were a binary operation, we could not apply it to the interval and get 1. Binary infimum is the same operation as binary min, and while the infimum of (1,2) is 1, the minimum value of (1,2) does not exist.

We can actually use this to do a much more direct proof of the associativity of binary min: binary min is the same thing as unary min (min as applied to a single set of arguments rather than two scalar arguments), and unary min cannot fail to be associative because it has only one argument. Repeated binary mins do nothing more than apply unary min to the set of individual arguments.

With no offense intended to the poster, the inferences are a little sloppy by mathematical standards and most of the hard work is done by introducing ("noticing") the set notation to the definition of min.

I agree. It's more of a sketch than a proof which is why it's so short.

Hence mathematicians will "hate it" and replace it with something more complicated and less clear

This proof works for any totally ordered set (hence a <= operation is defined on it)