for t, z being Integer holds
( t + z,t are_coprime iff t + z,z are_coprime ) by Lm6;