for a being non zero Nat
for b being odd Nat holds 2 |-count (a * b) = 2 |-count a