let i, j be natural Number ; :: thesis: ( j <= i implies max (0,(i - j)) = i - j )
assume j <= i ; :: thesis: max (0,(i - j)) = i - j
then j - j <= i - j by XREAL_1:9;
hence max (0,(i - j)) = i - j by XXREAL_0:def 10; :: thesis: verum