Bitwise operations on natural numbers
In the first half of this file, we provide theorems for reasoning about natural numbers from their
bitwise properties. In the second half of this file, we show properties of the bitwise operations
lxor, which are defined in core.
eq_of_test_bit_eq: two natural numbers are equal if they have equal bits at every position.
n ≠ 0, then there is some position
ithat contains the most significant
mare numbers and
iis a position such that the
i-th bit of of
nis zero, the
i-th bit of
mis one, and all more significant bits are equal, then
n < m.
There is another way to express bitwise properties of natural number:
digits 2. The two ways
should be connected.
bitwise, and, or, xor