let i, j, n be Nat; :: thesis: ( i < n & j < n & i,j are_congruent_mod n implies i = j )
assume A1: ( i < n & j < n & i,j are_congruent_mod n ) ; :: thesis: i = j
( i <= j or j < i ) ;
hence i = j by A1, INT_1:14, Lm6; :: thesis: verum