let i, j be Integer; :: thesis: (i mod j) mod j = i mod j

per cases ( j <> 0 or j = 0 ) ;

suppose j <> 0 ; :: thesis: (i mod j) mod j = i mod j

hence (i mod j) mod j = (i - ((i div j) * j)) mod j by INT_1:def 10
.= (i + (j * (- (i div j)))) mod j
.= i mod j by NAT_D:61 ;
:: thesis: verum

end;

suppose A1: j = 0 ; :: thesis: (i mod j) mod j = i mod j

hence (i mod j) mod j = 0 by INT_1:def 10
.= i mod j by A1, INT_1:def 10 ;
:: thesis: verum

end;

end;