lemma_u8_ilog2_ordered

vstd_extra::external::ilog2

Function lemma_u8_ilog2_ordered 

Source 
pub proof fn lemma_u8_ilog2_ordered(x: u8, y: u8)
Expand description
requires
x <= y,
ensures
x.ilog2() <= y.ilog2(),