A1: 2 is non trivial Nat by Def0;
a = (2 |^ (2 |-count a)) * (a / (2 |^ (2 |-count a))) by XCMPLX_1:87;
hence a / (2 |^ (2 |-count a)) is odd by A1, DX; :: thesis: verum