let j, i be Nat; :: 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:11;
hence max 0 ,(i - j) = i - j by XXREAL_0:def 10; :: thesis: verum