let n, m be Nat; :: thesis: ( n divides m implies n gcd m = n )
set N = n gcd m;
assume n divides m ; :: thesis: n gcd m = n
then A1: n divides n gcd m by NAT_D:def 5;
n gcd m divides n by NAT_D:def 5;
hence n gcd m = n by A1, NAT_D:5; :: thesis: verum