for R being commutative domRing-like Ring
for a being Element of R st a is_associated_to 0. R holds
a = 0. R