Function spec_range_inclusive_len 

pub open spec fn spec_range_inclusive_len<A: Step>(r: &RangeInclusive<A>) -> nat

{
    let steps = r@.start.spec_steps_between_int(r@.end);
    if steps >= 0 && !r@.exhausted { (steps + 1) as nat } else { 0 }
}

Number of elements left in an inclusive range: zero once it is exhausted or if start > end.