for t being Integer holds
( t is odd iff t gcd 2 = 1 )