let a be Element of NAT ; :: thesis: a gcd 0 = a
0 = 0 * a ;
then P2: a divides 0 by INT_1:def 3;
for m being Integer st m divides a & m divides 0 holds
m divides a ;
hence a gcd 0 = a by P2, INT_2:def 2; :: thesis: verum