n + 0 <= n + m by XREAL_1:6;
hence min ((n + m),n) = n by XXREAL_0:def 9; :: thesis: verum