for a, b, c being Nat st a <> 0 & c <> 0 & a,c are_coprime & b,c are_coprime holds
a * b,c are_coprime