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:21;
then (abs i) gcd (abs j) = abs i by NEWTON:62;
hence i gcd j = abs i by INT_2:51; :: thesis: verum