vstd::bits

Function lemma_u64_mul_pow2_le_max_iff_max_shr

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

Proof that for x, n and max of type u64 , 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.