let i, j be Integer; :: thesis: ( i divides j implies i gcd j = abs i )
assume i divides j ; :: thesis: i gcd j = abs i
then abs i divides abs j by INT_2:16;
then (abs i) gcd (abs j) = abs i by NEWTON:49;
hence i gcd j = abs i by INT_2:34; :: thesis: verum