theorem lemgcd0a: :: FIELD_14:42

for R being gcdDomain
for a being Element of R holds a is a_gcd of a, 0. R