theorem Th5: :: NUMBER13:5

for a, b, c being Nat st (a / b) * c is natural & b <> 0 & a,b are_coprime holds
ex d being Nat st c = b * d