pub broadcast proof fn axiom_range_inclusive_out_of_order<Idx: PartialOrd<Idx>>(
r: &RangeInclusive<Idx>,
)Expand description
ensures
Idx::obeys_partial_cmp_spec()
==> (#[trigger] spec_range_inclusive_out_of_order(r) <==> !r@.start.is_le(&r@.end)),