let a, b, n be Nat; :: thesis: ( a is odd & 2 |^ n divides a * b implies 2 |^ n divides b )
assume A1: ( a is odd & 2 |^ n divides a * b ) ; :: thesis: 2 |^ n divides b
then 2 |^ n,a are_coprime by NAT_5:3;
hence 2 |^ n divides b by A1, WSIERP_1:29; :: thesis: verum