let i, j be Element of NAT ; :: thesis: ( i <= j implies (0* j) | (i -' 1) = 0* (i -' 1) )
assume i <= j ; :: thesis: (0* j) | (i -' 1) = 0* (i -' 1)
then A2: i - 1 <= j - 1 by XREAL_1:11;
j - 1 <= j by XREAL_1:45;
then i - 1 <= j by A2, XXREAL_0:2;
then i -' 1 <= j by XREAL_0:def 2;
hence (0* j) | (i -' 1) = 0* (i -' 1) by Th1; :: thesis: verum