theorem :: PYTHTRIP:10

for a, b being Element of NAT holds
( not a,b are_coprime or a is odd or b is odd ) ;