lemma_usize_ilog2_ordered

vstd_extra::external::ilog2

Function lemma_usize_ilog2_ordered 

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