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