Function borrowed_key_ordering_matches 

pub open spec fn borrowed_key_ordering_matches<T: Borrow<U> + Ord, U: Ord + ?Sized>() -> bool

{
    forall |x: T, y: T| {
        #[trigger] x.cmp_spec(&y)
            == <T as BorrowSpec<U>>::borrow_spec(&x)
                .cmp_spec(<T as BorrowSpec<U>>::borrow_spec(&y))
    }
}

Whether borrowing preserves the ordering of values.

This compares the cmp_spec results; faithfulness of the comparison and borrowing specifications is expressed separately by their obeys_*_spec predicates.