for t, z being Integer holds
( t gcd z is even iff ( t is even & z is even ) )