for a, b, c being Integer st c <> 0 & a = b mod c & b,c are_coprime holds
a,c are_coprime