theorem :: GAUSSINT:44

for x, y being G_INTEG st Re y <> 0 & Im y <> 0 & Re y <> Im y & - (Re y) <> Im y & x *' is_associated_to y holds
( not x Divides y & not y Divides x )