pub open spec fn finite_range_matches_ord<T: FiniteRange + Ord>() -> bool
{ forall |x: T, lo: T, hi: T| T::in_range(x, lo, hi) <==> lo.is_le(&x) && x.is_lt(&hi) }
Whether the finite-range model agrees with the ordering model.