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