let k, m, n be Integer; :: thesis: ( k mod n = m mod n implies (k - m) mod n = 0 )
assume A1: k mod n = m mod n ; :: thesis: (k - m) mod n = 0

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

suppose A2: n <> 0 ; :: thesis: (k - m) mod n = 0

then k - ((k div n) * n) = m mod n by A1, INT_1:def 10
.= m - ((m div n) * n) by A2, INT_1:def 10 ;
then k - m = n * ((k div n) - (m div n)) ;
hence (k - m) mod n = 0 by Lm18; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (k - m) mod n = 0

hence (k - m) mod n = 0 by INT_1:def 10; :: thesis: verum

end;

end;