theorem :: PYTHTRIP:10

for a, b being Nat holds
( not a,b are_coprime or a is odd or b is odd ) ;