let i be integer number ; :: thesis: for j being non zero integer number holds i,i mod j are_congruent_mod j
let j be non zero integer number ; :: thesis: i,i mod j are_congruent_mod j
i = ((i div j) * j) + (i mod j) by INT_1:59;
hence i,i mod j are_congruent_mod j ; :: thesis: verum