vstd::bits

Function lemma_u16_mul_pow2_le_max_iff_max_shr

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

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