let a, b be non zero Integer; :: thesis: ( Parity a, Oddity b are_coprime & (Parity a) gcd (Oddity b) = 1 )
(Oddity b) gcd 2 = 1 by NEWTON03:def 5;
then (Oddity b) gcd (2 |^ (2 |-count a)) = 1 by WSIERP_1:12;
hence ( Parity a, Oddity b are_coprime & (Parity a) gcd (Oddity b) = 1 ) by Def1; :: thesis: verum