let t, z be Integer; :: thesis: ( t + z,z are_coprime implies t + z,t are_coprime )
assume t + z,z are_coprime ; :: thesis: t + z,t are_coprime
then 1 = (t + (1 * z)) gcd z
.= t gcd z by Th5
.= (z + (1 * t)) gcd t by Th5 ;
hence t + z,t are_coprime ; :: thesis: verum