Function spec_range_inclusive_is_empty 

pub open spec fn spec_range_inclusive_is_empty<Idx: PartialOrd<Idx>>(
    r: &RangeInclusive<Idx>,
) -> bool

{ !r@.start.is_le(&r@.end) || r@.exhausted }