let i, j be Integer; :: thesis: ( i,j are_congruent_mod j implies i, 0 are_congruent_mod j )
j, 0 are_congruent_mod j ;
hence ( i,j are_congruent_mod j implies i, 0 are_congruent_mod j ) by INT_1:15; :: thesis: verum