let m be Nat; :: thesis: m gcd 0 = m
set M = m gcd 0 ;
A1: m divides m gcd 0

proof

m divides 0 by NAT_D:6;
hence m divides m gcd 0 by NAT_D:def 5; :: thesis: verum

end;

m gcd 0 divides m by NAT_D:def 5;
hence m gcd 0 = m by A1, NAT_D:5; :: thesis: verum