lemma_u32_ilog2_ordered

vstd_extra::external::ilog2

Function lemma_u32_ilog2_ordered 

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