let i be Integer; :: thesis: for j being non zero Integer holds i,i mod j are_congruent_mod j
let j be non zero Integer; :: 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