Function vstd::set_lib::lemma_int_range

source · 
pub proof fn lemma_int_range(lo: int, hi: int)
Expand description
requires
lo <= hi,
ensures
set_int_range(lo, hi).finite(),
set_int_range(lo, hi).len() == hi - lo,

If a set solely contains integers in the range [a, b), then its size is bounded by b - a.