let a, b, c be Integer; :: thesis: ( c <> 0 & a = b mod c & b,c are_coprime implies a,c are_coprime )
assume A1: ( c <> 0 & a = b mod c & b,c are_coprime ) ; :: thesis: a,c are_coprime
then b gcd c = 1 by INT_2:def 3;
then a gcd c = 1 by A1, Th8, WSIERP_1:43;
hence a,c are_coprime by INT_2:def 3; :: thesis: verum