let a, b, m be Integer; :: thesis: ( not a,b are_congruent_mod m or not m divides a or m divides b )
assume ( a,b are_congruent_mod m & m divides a ) ; :: thesis: m divides b
then m divides a - (a - b) by INT_5:1;
hence m divides b ; :: thesis: verum