lemma_u16_ilog2_ordered

vstd_extra::external::ilog2

Function lemma_u16_ilog2_ordered 

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