theorem Th1: :: GCD_1:1

for R being commutative domRing-like Ring
for a, b, c being Element of R st a <> 0. R holds
( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) )