theorem :: NAT_D:32

for i being natural Number holds i gcd i = i