lemma_usize_shr_is_div

vstd::bits

Function lemma_usize_shr_is_div 

Source 
pub broadcast proof fn lemma_usize_shr_is_div(x: usize, shift: usize)
Expand description
requires
0 <= shift < <usize>::BITS,
ensures
#[trigger] (x >> shift) == x as nat / pow2(shift as nat),

Proof that for x and n of type usize , shifting x right by n is equivalent to division of x by 2^n.