theorem Th3: :: FINSEQ_2:4

for i, j being natural Number st j <= i holds
max (0,(i - j)) = i - j