let i, j be Nat; :: thesis: ( 0 < j & j <= i & i < j + j implies ( i mod j = i - j & i mod j = i -' j ) )
assume A1: ( 0 < j & j <= i & i < j + j ) ; :: thesis: ( i mod j = i - j & i mod j = i -' j )
then A2: i - j = i -' j by XREAL_1:235;
i = (i - j) + j ;
then A3: i mod j = ((i -' j) + j) mod j by A1, XREAL_1:235
.= ((i -' j) + (j mod j)) mod j by NAT_D:23
.= ((i -' j) + 0 ) mod j by NAT_D:25
.= (i -' j) mod j ;
i - j < (j + j) - j by A1, XREAL_1:11;
hence ( i mod j = i - j & i mod j = i -' j ) by A2, A3, NAT_D:24; :: thesis: verum