vstd::bits

Function lemma_low_bits_mask_is_odd

Source 
pub broadcast proof fn lemma_low_bits_mask_is_odd(n: nat)
Expand description
requires
n > 0,
ensures
#[trigger] (low_bits_mask(n) % 2) == 1,

Proof that low_bits_mask(n) is odd.