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