vstd::bits

Function lemma_u8_mul_pow2_le_max_iff_max_shr

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

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