lemma_u64_ilog2_ordered

vstd_extra::external::ilog2

Function lemma_u64_ilog2_ordered 

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