let i, j be Nat; :: thesis: ( i <= j implies (0* j) | (i -' 1) = 0* (i -' 1) )
assume i <= j ; :: thesis: (0* j) | (i -' 1) = 0* (i -' 1)
then A1: i - 1 <= j - 1 by XREAL_1:9;
j - 1 <= j by XREAL_1:43;
then i - 1 <= j by A1, XXREAL_0:2;
then i -' 1 <= j by XREAL_0:def 2;
hence (0* j) | (i -' 1) = 0* (i -' 1) by Th1; :: thesis: verum