lemma_usize_log2_bounds

vstd_extra::external::ilog2

Function lemma_usize_log2_bounds 

Source 
pub proof fn lemma_usize_log2_bounds(x: usize)
Expand description
ensures
0 <= log(2, x as int) <= usize::BITS,
0 <= x.ilog2() <= usize::BITS,