Function vstd::bits::lemma_u32_shr_is_div
source · pub broadcast proof fn lemma_u32_shr_is_div(x: u32, shift: u32)Expand description
requires
0 <= shift < <u32>::BITS,#[trigger] (x >> shift) == x as nat / pow2(shift as nat),Proof that for x and n of type u32 , shifting x right by n is equivalent to division of x by 2^n.