let m be Nat; :: thesis: m gcd 0 = m
set M = m gcd 0;
m divides 0 by NAT_D:6;
then A1: m divides m gcd 0 by NAT_D:def 5;
m gcd 0 divides m by NAT_D:def 5;
hence m gcd 0 = m by A1, NAT_D:5; :: thesis: verum