theorem :: INT_2:23

for a, b being Integer st ( a <> 0 or b <> 0 ) holds
ex a1, b1 being Integer st
( a = (a gcd b) * a1 & b = (a gcd b) * b1 & a1,b1 are_coprime )