let a, b be Integer; :: thesis: ( not a,b are_coprime or a is odd or b is odd )
assume A1: a,b are_coprime ; :: thesis: ( a is odd or b is odd )
assume ( not a is odd & not b is odd ) ; :: thesis: contradiction
then a gcd b is even ;
hence contradiction by A1; :: thesis: verum