for a being non zero Nat ex k being odd Nat st a = (2 |^ (2 |-count a)) * k