for n, i being Nat st 0 <= i & i < 2 |^ n holds
((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)