Function borrowed_key_ordering_matches 

pub uninterp spec fn borrowed_key_ordering_matches<Key: Borrow<Q> + Ord, Q: Ord + ?Sized>() -> bool

Whether a borrowed key type’s ordering agrees with the ordering of stored keys.

This is the semantic requirement imposed on Key: Borrow<Q> by the standard library’s borrowed-key BTreeMap operations.