let a, b be Nat; :: thesis: ( a is odd & a gcd b = 1 implies a gcd (2 * b) = 1 )
assume A1: ( a is odd & a gcd b = 1 ) ; :: thesis: a gcd (2 * b) = 1
then A2: a,b are_coprime ;
a,2 |^ 1 are_coprime by A1, NAT_5:3;
then a,2 * b are_coprime by A2, INT_2:26;
hence a gcd (2 * b) = 1 ; :: thesis: verum