Function vstd::bits::lemma_low_bits_mask_div2

source · 
pub broadcast proof fn lemma_low_bits_mask_div2(n: nat)
Expand description
requires
n > 0,
ensures
#[trigger] (low_bits_mask(n) / 2) == low_bits_mask((n - 1) as nat),

Proof that dividing the low n bit mask by 2 gives the low n-1 bit mask.