let i, j be Nat; :: thesis: ( j <= i & i < j + j implies ( i mod j = i - j & i mod j = i -' j ) )
assume that
A1: j <= i and
A2: i < j + j ; :: thesis: ( i mod j = i - j & i mod j = i -' j )
A3: i - j < (j + j) - j by A2, XREAL_1:9;
i = (i - j) + j ;
then A4: i mod j = ((i -' j) + j) mod j by A1, XREAL_1:233
.= ((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 = i -' j by A1, XREAL_1:233;
hence ( i mod j = i - j & i mod j = i -' j ) by A4, A3, NAT_D:24; :: thesis: verum