let n, m be Nat; :: 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 NAT_D:def 5;
( n gcd m = 0 or n gcd m < 0 ) by A2;
then ex r being Nat st n = 0 * r by A3, NAT_D:def 3;
hence contradiction by A1; :: thesis: verum