lemma_u16_log2_bounds

vstd_extra::external::ilog2

Function lemma_u16_log2_bounds 

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