lemma_u8_log2_bounds

vstd_extra::external::ilog2

Function lemma_u8_log2_bounds 

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