vstd::bits

Function lemma_u32_mul_pow2_le_max_iff_max_shr

Source 
pub proof fn lemma_u32_mul_pow2_le_max_iff_max_shr(x: u32, shift: u32, max: u32)
Expand description
requires
0 <= shift < <u32>::BITS,
ensures
x * pow2(shift as nat) <= max <==> x <= (max >> shift),

Proof that for x, n and max of type u32 , multiplication of x by 2^n is less than or equal to max if and only if x is less than or equal to shifting max right by n.