let m, n be Integer; :: thesis: ( n > 0 implies n gcd m > 0 )
assume that
A1: n > 0 and
A2: n gcd m <= 0 ; :: thesis: contradiction
A3: n gcd m divides n by INT_2:def 2;
( n gcd m = 0 or n gcd m < 0 ) by A2;
then ex r being Integer st n = 0 * r by A3, INT_1:def 3;
hence contradiction by A1; :: thesis: verum