for L being gcdDomain
for x, y being Element of L
for u, v being a_gcd of x,y holds u is_associated_to v