Function lemma_usize_mul_pow2_le_max_iff_max_shr 

pub proof fn lemma_usize_mul_pow2_le_max_iff_max_shr(
    x: usize,
    shift: usize,
    max: usize,
)

requires

0 <= shift < <usize>::BITS,

ensures

x * pow2(shift as nat) <= max <==> x <= (max >> shift),

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