pub proof fn lemma_int_range(lo: int, hi: int)Expand description
requires
lo <= hi,forall |j: int| set_int_range(lo, hi).contains(j) <==> lo <= j < hi,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.